# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1306840948 -3600
# Node ID 3e341af86bbd98ef03393b04673ea3493f3fea76
# Parent  929bd2dd1ab2bfb68a522a51d3d41abf7fb97a30
fixed the problem with cps-like functions

diff -r 929bd2dd1ab2 -r 3e341af86bbd Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue May 31 14:12:31 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Tue May 31 12:22:28 2011 +0100
@@ -10,7 +10,6 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
-
 inductive 
   triv :: "lam \<Rightarrow> nat \<Rightarrow> bool"
 where
@@ -563,24 +562,22 @@
 apply(rule refl)
 oops
 
-text {* not working yet *}
+text {* "HO" functions *}
 
-(* not working yet
 nominal_primrec
-  trans :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
+  trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
 where
-  "trans (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))"
-| "trans (App t1 t2) xs = ((trans t1 xs) \<guillemotright>= (\<lambda>db1. (trans t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))"
-| "trans (Lam [x].t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
-*)
+  "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))"
+| "trans2 (App t1 t2) xs = ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))"
+| "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
+oops
 
-(* not working yet
 nominal_primrec
   CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
 where
   "CPS (Var x) k = Var x"
 | "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))"
-*)
+oops
 
 
 (* function tests *)
diff -r 929bd2dd1ab2 -r 3e341af86bbd Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Tue May 31 14:12:31 2011 +0900
+++ b/Nominal/nominal_function_core.ML	Tue May 31 12:22:28 2011 +0100
@@ -336,7 +336,7 @@
     fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = 
         (llRI RS ih_eqvt_case)
         |> fold_rev (Thm.implies_intr o cprop_of) CCas
-        |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+        (* fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs *)
   in
     map prep_eqvt RCs
     |> map (fold_rev (Thm.implies_intr o cprop_of) ags)