# HG changeset patch
# User bulwahn
# Date 1258013506 -3600
# Node ID 68e058d061f518c59a62f6606db6131d2619ccde
# Parent  5f35cf91c6a43830c47dc73c22c1d33b9ad7e10e
removed unnecessary oracle in the predicate compiler

diff -r 5f35cf91c6a4 -r 68e058d061f5 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Nov 12 09:11:41 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Nov 12 09:11:46 2009 +0100
@@ -151,7 +151,7 @@
       Predicate_Compile_Core.code_pred_cmd options raw_const lthy
   end
 
-val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
+val setup = Predicate_Compile_Core.setup
 
 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
   "show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited",
diff -r 5f35cf91c6a4 -r 68e058d061f5 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Nov 12 09:11:41 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Nov 12 09:11:46 2009 +0100
@@ -6,29 +6,14 @@
 
 signature PREDICATE_COMPILE_FUN =
 sig
-val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory
+  val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory
   val rewrite_intro : theory -> thm -> thm list
-  val setup_oracle : theory -> theory
   val pred_of_function : theory -> string -> string option
 end;
 
 structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN =
 struct
 
-
-(* Oracle for preprocessing  *)
-
-val (oracle : (string * (cterm -> thm)) option Unsynchronized.ref) = Unsynchronized.ref NONE;
-
-fun the_oracle () =
-  case !oracle of
-    NONE => error "Oracle is not setup"
-  | SOME (_, oracle) => oracle
-             
-val setup_oracle = Thm.add_oracle (Binding.name "pred_compile_preprocessing", I) #->
-  (fn ora => fn thy => let val _ = (oracle := SOME ora) in thy end)
-  
-  
 fun is_funtype (Type ("fun", [_, _])) = true
   | is_funtype _ = false;
 
@@ -393,9 +378,6 @@
           in ([], thy) end
   end
 
-(* preprocessing intro rules - uses oracle *)
-
-(* theory -> thm -> thm *)
 fun rewrite_intro thy intro =
   let
     fun lookup_pred (Const (name, T)) =
@@ -435,7 +417,7 @@
         |> map (fn (concl'::conclprems, _) =>
           Logic.list_implies ((flat prems') @ conclprems, concl')))
   in
-    map (Drule.standard o the_oracle () o cterm_of thy) intro_ts'
-  end; 
+    map (Drule.standard o (Skip_Proof.make_thm thy)) intro_ts'
+  end
 
 end;