# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1282708717 -28800
# Node ID 7aa18bae69839384cfb1510fdd905e83d6c24726
# Parent  331873ebc5cd51f1e5f0976db8366ccaff895c2b
now every lemma lifts (even with type variables)

diff -r 331873ebc5cd -r 7aa18bae6983 Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Wed Aug 25 09:02:06 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Wed Aug 25 11:58:37 2010 +0800
@@ -110,7 +110,6 @@
   val _ = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct})
 *}
 
-
 ML {* 
   val _ = timeit (fn () => map (lift_thm @{context} qtys []) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.induct})
 *}
diff -r 331873ebc5cd -r 7aa18bae6983 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Aug 25 09:02:06 2010 +0800
+++ b/Nominal/Ex/Lambda.thy	Wed Aug 25 11:58:37 2010 +0800
@@ -68,8 +68,6 @@
     prod.cases}
 *}
 
-(*  HERE *)
-
 ML {*
  val thms_e = map (lift_thm @{context} qtys simps)  @{thms eq_iff}
 *}
@@ -97,12 +95,6 @@
 
 
 
-ML {*
-  space_explode "_raw" "bla_raw2_foo_raw3.0"
-*}
-
-
-
 thm eq_iff
 
 thm lam.fv
diff -r 331873ebc5cd -r 7aa18bae6983 Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Wed Aug 25 09:02:06 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Wed Aug 25 11:58:37 2010 +0800
@@ -123,12 +123,16 @@
 end
 
 fun lift_thm ctxt qtys simps thm =
-  thm
-  |> Quotient_Tacs.lifted ctxt qtys simps
+let
+  val ((_, [thm']), ctxt') = Variable.importT [thm] ctxt
+in
+  thm'
+  |> Quotient_Tacs.lifted ctxt' qtys simps
+  |> singleton (ProofContext.export ctxt' ctxt) 
   |> unraw_bounds_thm
   |> unraw_vars_thm
   |> Drule.zero_var_indexes
-
+end
 
 end (* structure *)