# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255506613 -7200
# Node ID 19c662f8b9d6bb3902a836bc4b5876e59c7ab94f
# Parent  072f2f8dc694e3620825b715a01052b75b61e6c9# Parent  19d3856abb81d1a426037b55609780566a5582b1
Merge

diff -r 19d3856abb81 -r 19c662f8b9d6 QuotMain.thy
--- a/QuotMain.thy	Tue Oct 13 22:22:15 2009 +0200
+++ b/QuotMain.thy	Wed Oct 14 09:50:13 2009 +0200
@@ -358,7 +358,7 @@
       in
         Term.lambda_name (x, v) rec_term
       end
-  | ((Const (@{const_name "All"}, _)) $ (Abs (x, T, t))) =>
+  | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) =>
       if T = rty then let
         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
         val v = Free (x', rty);
@@ -378,10 +378,11 @@
         val v = Free (x', rty);
         val t' = subst_bound (v, t);
         val rec_term = regularise t' rty rel lthy2;
+        val lam_term = Term.lambda_name (x, v) rec_term
       in
-        Term.lambda_name (x, v) rec_term
+        Const(@{const_name "All"}, at) $ lam_term
       end
-  | ((Const (@{const_name "Ex"}, _)) $ (Abs (x, T, t))) =>
+  | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
       if T = rty then let
         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
         val v = Free (x', rty);
@@ -401,9 +402,11 @@
         val v = Free (x', rty);
         val t' = subst_bound (v, t);
         val rec_term = regularise t' rty rel lthy2;
+        val lam_term = Term.lambda_name (x, v) rec_term
       in
-        Term.lambda_name (x, v) rec_term
+        Const(@{const_name "All"}, at) $ lam_term
       end
+  | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)
   | _ => trm
 
 *}
@@ -1110,10 +1113,17 @@
 
 thm list.induct
 
-ML {* val li = atomize_thm @{thm list.induct} *}
+ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
 
-ML {* (* Doesn't recognize that 'a list = '?a list *)
-  cterm_of @{theory} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})
+ML {*
+Syntax.string_of_term @{context}  (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})
+|> writeln
+*}
+
+ML {*
+  Toplevel.program (fn () =>
+cterm_of @{theory} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})
+  )
 *}