# HG changeset patch
# User wenzelm
# Date 1244723158 -7200
# Node ID ac0badf13d934c29b17766681f3851afd8b0963d
# Parent  318081898306009dc57eb8387ad22d8ec0dec8cd# Parent  995d6b90e9d6a326d91ba0db2400735cf966d36d
merged, reverting workarounds on both sides;

diff -r 318081898306 -r ac0badf13d93 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Thu Jun 11 12:50:20 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Thu Jun 11 14:25:58 2009 +0200
@@ -44,13 +44,15 @@
   | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
   | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
 
+(* FIXME: correct handling of parameters *)
+(*
 ML {* reset Predicate_Compile.do_proofs *}
-
 code_pred partition .
 
 thm partition.equation
+ML {* set Predicate_Compile.do_proofs *}
+*)
 
-ML {* set Predicate_Compile.do_proofs *}
 (* TODO: requires to handle abstractions in parameter positions correctly *)
 (*FIXME values 10 "{(ys, zs). partition (\<lambda>n. n mod 2 = 0)
   [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}" *)
@@ -63,11 +65,11 @@
 "r a b ==> tranclp r b c ==> tranclp r a c" 
 by auto
 *)
-
+(*
 code_pred tranclp .
 
 thm tranclp.equation
-
+*)
 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
     "succ 0 1"
   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
diff -r 318081898306 -r ac0badf13d93 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Jun 11 12:50:20 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Jun 11 14:25:58 2009 +0200
@@ -14,11 +14,10 @@
   "Codegenerator_Pretty_Test",
   "NormalForm",
   "../NumberTheory/Factorization",
-  "Predicate_Compile"
+  "Predicate_Compile",
+  "Predicate_Compile_ex"
 ];
 
-setmp quick_and_dirty true use_thy "Predicate_Compile_ex";
-
 use_thys [
   "Numeral",
   "Higher_Order_Logic",
diff -r 318081898306 -r ac0badf13d93 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Thu Jun 11 12:50:20 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Thu Jun 11 14:25:58 2009 +0200
@@ -1445,13 +1445,15 @@
 (* TODO: must create state to prove multiple cases *)
 fun generic_code_pred prep_const raw_const lthy =
   let
+  
     val thy = ProofContext.theory_of lthy
     val const = prep_const thy raw_const
+    
     val lthy' = LocalTheory.theory (PredData.map (Graph.extend (dependencies_of thy) const)) lthy
       |> LocalTheory.checkpoint
     val thy' = ProofContext.theory_of lthy'
     val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy')
-    val _ = Output.tracing ("preds: " ^ commas preds)
+    
     fun mk_cases const =
       let
         val nparams = nparams_of thy' const