# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272973960 -7200
# Node ID 5098771ff041a4449d4b7c429d19176116d3f97c
# Parent  495b6feb76a8f67d4da890abd6d94206a5157638
ExPS7 in NewParser

diff -r 495b6feb76a8 -r 5098771ff041 Nominal/Ex/ExPS7.thy
--- a/Nominal/Ex/ExPS7.thy	Tue May 04 12:34:33 2010 +0200
+++ b/Nominal/Ex/ExPS7.thy	Tue May 04 13:52:40 2010 +0200
@@ -1,17 +1,16 @@
 theory ExPS7
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* example 7 from Peter Sewell's bestiary *)
 
 atom_decl name
 
-ML {* val _ = recursive := true  *}
 nominal_datatype exp7 =
   EVar name
 | EUnit
 | EPair exp7 exp7
-| ELetRec l::"lrbs" e::"exp7" bind "b7s l" in e
+| ELetRec l::"lrbs" e::"exp7" bind_set "b7s l" in l e
 and lrb =
   Assign name exp7
 and lrbs =