# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272982941 -7200
# Node ID ca512f9c0b0ab8ed24fe7d581ed72350f25d03db
# Parent  6800fcaafa2afa446eecea69fb14d33134596a0a
Move ExPS8 to new parser.

diff -r 6800fcaafa2a -r ca512f9c0b0a Nominal/Ex/ExPS8.thy
--- a/Nominal/Ex/ExPS8.thy	Tue May 04 14:21:18 2010 +0200
+++ b/Nominal/Ex/ExPS8.thy	Tue May 04 16:22:21 2010 +0200
@@ -1,23 +1,21 @@
 theory ExPS8
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* example 8 from Peter Sewell's bestiary *)
 
 atom_decl name
 
-(* One function is recursive and the other one is not,
-   and as the parser cannot handle this we cannot set
-   the reference.  *)
-ML {* val _ = recursive := false  *}
+ML {* val _ = cheat_fv_rsp := true *}
+ML {* val _ = cheat_alpha_bn_rsp := true *}
 
 nominal_datatype exp =
   EVar name
 | EUnit
 | EPair exp exp
-| ELetRec l::lrbs e::exp bind "b_lrbs l" in e (* rec *)
+| ELetRec l::lrbs e::exp bind_set "b_lrbs l" in l e
 and fnclause =
-  K x::name p::pat f::exp bind "b_pat p" in f (* non-rec *)
+  K x::name p::pat f::exp bind_set "b_pat p" in f
 and fnclauses =
   S fnclause
 | ORs fnclause fnclauses
@@ -47,8 +45,8 @@
 | "b_lrb (Clause fcs) = (b_fnclauses fcs)"
 | "b_fnclause (K x pat exp) = {atom x}"
 
-thm exp7_lrb_lrbs.eq_iff
-thm exp7_lrb_lrbs.supp
+thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv
+thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff
 
 end