# HG changeset patch
# User bulwahn
# Date 1284389057 -7200
# Node ID 17ef4415b17c74bbdae3ca7319027e75a171d73e
# Parent  74469faa27cac685908f9e65475dc239e2e32e57
removing obsolete argument in prepare_intrs; passing context instead of theory in prepare_intrs

diff -r 74469faa27ca -r 17ef4415b17c src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Sep 13 15:22:40 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Sep 13 16:44:17 2010 +0200
@@ -63,12 +63,12 @@
   val add_random_dseq_equations : options -> string list -> theory -> theory
   val add_new_random_dseq_equations : options -> string list -> theory -> theory
   val mk_tracing : string -> term -> term
-  val prepare_intrs : options -> compilation -> theory -> string list -> thm list ->
+  val prepare_intrs : options -> Proof.context -> string list -> thm list ->
     ((string * typ) list * string list * string list * (string * mode list) list *
       (string *  (Term.term list * Predicate_Compile_Aux.indprem list) list) list)
   type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool}  
   datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
-  | Mode_Pair of mode_derivation * mode_derivation | Term of mode
+    | Mode_Pair of mode_derivation * mode_derivation | Term of mode
   type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list
   type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
 
@@ -2684,9 +2684,9 @@
     if is_registered ctxt s then Prem t else Sidecond t
   | _ => Sidecond t)
 
-fun prepare_intrs options compilation thy prednames intros =
+fun prepare_intrs options ctxt prednames intros =
   let
-    val ctxt = ProofContext.init_global thy
+    val thy = ProofContext.theory_of ctxt
     val intrs = map prop_of intros
     val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames
     val (preds, intrs) = unify_consts thy preds intrs
@@ -2842,7 +2842,7 @@
         tracing (commas (map (Display.string_of_thm ctxt) (maps (intros_of ctxt) prednames)))
       else ()
     val (preds, all_vs, param_vs, all_modes, clauses) =
-      prepare_intrs options compilation thy prednames (maps (intros_of ctxt) prednames)
+      prepare_intrs options ctxt prednames (maps (intros_of ctxt) prednames)
     val _ = print_step options "Infering modes..."
     val (lookup_mode, lookup_neg_mode, needs_random) = (modes_of compilation ctxt,
       modes_of (negative_compilation_of compilation) ctxt, needs_random ctxt)