# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255506436 -7200
# Node ID 072f2f8dc694e3620825b715a01052b75b61e6c9
# Parent  9220c51e5155f5e9e20dc7eedf58d95c9a3ebfc9
Proper handling of non-lifted quantifiers, testing type freezing.

diff -r 9220c51e5155 -r 072f2f8dc694 QuotMain.thy
--- a/QuotMain.thy	Tue Oct 13 18:01:54 2009 +0200
+++ b/QuotMain.thy	Wed Oct 14 09:47:16 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
 
 *}
@@ -1116,10 +1119,17 @@
 
 thm list.induct
 
-ML {* val li = atomize_thm (meta_quantify @{thm list.induct}) *}
+ML {* val li = Thm.freezeT (atomize_thm (meta_quantify @{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})
+  )
 *}