# HG changeset patch
# User bulwahn
# Date 1249367696 -7200
# Node ID bca7fd8498297d3684f15591b2c1dfe463150799
# Parent  b4b871808223ceff264f69b18ac0c800f08e6310
improved use of context with cases rule in predicate compiler; predicate compiler based on Main for faster debugging

diff -r b4b871808223 -r bca7fd849829 src/HOL/ex/Predicate_Compile.thy
--- 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
 
diff -r b4b871808223 -r bca7fd849829 src/HOL/ex/Predicate_Compile_ex.thy
--- 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
diff -r b4b871808223 -r bca7fd849829 src/HOL/ex/predicate_compile.ML
--- 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;