improved use of context with cases rule in predicate compiler; predicate compiler based on Main for faster debugging

--- a/src/HOL/ex/Predicate_Compile.thy	Tue Aug 04 08:34:56 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Tue Aug 04 08:34:56 2009 +0200
@@ -1,5 +1,5 @@
 theory Predicate_Compile
-imports Complex_Main Lattice_Syntax Code_Eval RPred
+imports Main Lattice_Syntax Code_Eval RPred
 uses "predicate_compile.ML"
 begin
 

--- a/src/HOL/ex/Predicate_Compile_ex.thy	Tue Aug 04 08:34:56 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Tue Aug 04 08:34:56 2009 +0200
@@ -1,5 +1,5 @@
 theory Predicate_Compile_ex
-imports Complex_Main Predicate_Compile
+imports Main Predicate_Compile
 begin
 
 inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where

--- a/src/HOL/ex/predicate_compile.ML	Tue Aug 04 08:34:56 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Tue Aug 04 08:34:56 2009 +0200
@@ -2053,10 +2053,16 @@
         assumes = [("", Logic.strip_imp_prems case_rule)],
         binds = [], cases = []}) cases_rules
     val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
-    val lthy'' = ProofContext.add_cases true case_env lthy'
-    
-    fun after_qed thms =
-      LocalTheory.theory (fold set_elim (map the_single thms) #> add_equations [const])
+    val lthy'' = lthy'
+      |> fold Variable.auto_fixes cases_rules 
+      |> ProofContext.add_cases true case_env
+    fun after_qed thms goal_ctxt =
+      let
+        val global_thms = ProofContext.export goal_ctxt
+          (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms)
+      in
+        goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #> add_equations [const])
+      end  
   in
     Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
   end;