1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:06 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:07 2010 +0200
     1.3 @@ -326,9 +326,9 @@
     1.4    (map (string_of_prem ctxt) prems)) ^ " --> " ^ pred ^ " "
     1.5     ^ (space_implode " " (map (Syntax.string_of_term ctxt) ts))
     1.6  
     1.7 -fun print_compiled_terms options thy =
     1.8 +fun print_compiled_terms options ctxt =
     1.9    if show_compilation options then
    1.10 -    print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy
    1.11 +    print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term ctxt)
    1.12    else K ()
    1.13  
    1.14  fun print_stored_rules thy =
    1.15 @@ -1821,7 +1821,7 @@
    1.16  
    1.17  (** switch detection analysis **)
    1.18  
    1.19 -fun find_switch_test thy (i, is) (ts, prems) =
    1.20 +fun find_switch_test ctxt (i, is) (ts, prems) =
    1.21    let
    1.22      val t = nth_pair is (nth ts i)
    1.23      val T = fastype_of t
    1.24 @@ -1829,7 +1829,7 @@
    1.25      case T of
    1.26        TFree _ => NONE
    1.27      | Type (Tcon, _) =>
    1.28 -      (case Datatype_Data.get_constrs thy Tcon of
    1.29 +      (case Datatype_Data.get_constrs (ProofContext.theory_of ctxt) Tcon of
    1.30          NONE => NONE
    1.31        | SOME cs =>
    1.32          (case strip_comb t of
    1.33 @@ -1838,11 +1838,11 @@
    1.34          | (Const (c, T), _) => if AList.defined (op =) cs c then SOME (c, T) else NONE))
    1.35    end
    1.36  
    1.37 -fun partition_clause thy pos moded_clauses =
    1.38 +fun partition_clause ctxt pos moded_clauses =
    1.39    let
    1.40      fun insert_list eq (key, value) = AList.map_default eq (key, []) (cons value)
    1.41      fun find_switch_test' moded_clause (cases, left) =
    1.42 -      case find_switch_test thy pos moded_clause of
    1.43 +      case find_switch_test ctxt pos moded_clause of
    1.44          SOME (c, T) => (insert_list (op =) ((c, T), moded_clause) cases, left)
    1.45        | NONE => (cases, moded_clause :: left)
    1.46    in
    1.47 @@ -1852,12 +1852,12 @@
    1.48  datatype switch_tree =
    1.49    Atom of moded_clause list | Node of (position * ((string * typ) * switch_tree) list) * switch_tree
    1.50  
    1.51 -fun mk_switch_tree thy mode moded_clauses =
    1.52 +fun mk_switch_tree ctxt mode moded_clauses =
    1.53    let
    1.54      fun select_best_switch moded_clauses input_position best_switch =
    1.55        let
    1.56          val ord = option_ord (rev_order o int_ord o (pairself (length o snd o snd)))
    1.57 -        val partition = partition_clause thy input_position moded_clauses
    1.58 +        val partition = partition_clause ctxt input_position moded_clauses
    1.59          val switch = if (length (fst partition) > 1) then SOME (input_position, partition) else NONE
    1.60        in
    1.61          case ord (switch, best_switch) of LESS => best_switch
    1.62 @@ -1945,9 +1945,8 @@
    1.63  
    1.64  (* compilation of predicates *)
    1.65  
    1.66 -fun compile_pred options compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
    1.67 +fun compile_pred options compilation_modifiers ctxt all_vs param_vs s T (pol, mode) moded_cls =
    1.68    let
    1.69 -    val ctxt = ProofContext.init_global thy
    1.70      val compilation_modifiers = if pol then compilation_modifiers else
    1.71        negative_comp_modifiers_of compilation_modifiers
    1.72      val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
    1.73 @@ -1975,7 +1974,7 @@
    1.74        if detect_switches options then
    1.75          the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs))
    1.76            (compile_switch compilation_modifiers ctxt all_vs param_vs additional_arguments
    1.77 -            mode in_ts' outTs (mk_switch_tree thy mode moded_cls))
    1.78 +            mode in_ts' outTs (mk_switch_tree ctxt mode moded_cls))
    1.79        else
    1.80          let
    1.81            val cl_ts =
    1.82 @@ -2643,8 +2642,8 @@
    1.83    map (fn (pred, modes) =>
    1.84      (pred, map (fn (mode, value) => value) modes)) preds_modes_table
    1.85  
    1.86 -fun compile_preds options comp_modifiers thy all_vs param_vs preds moded_clauses =
    1.87 -  map_preds_modes (fn pred => compile_pred options comp_modifiers thy all_vs param_vs pred
    1.88 +fun compile_preds options comp_modifiers ctxt all_vs param_vs preds moded_clauses =
    1.89 +  map_preds_modes (fn pred => compile_pred options comp_modifiers ctxt all_vs param_vs pred
    1.90        (the (AList.lookup (op =) preds pred))) moded_clauses
    1.91  
    1.92  fun prove options thy clauses preds moded_clauses compiled_terms =
    1.93 @@ -2838,12 +2837,13 @@
    1.94        Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..."
    1.95        (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy'
    1.96        |> Theory.checkpoint)
    1.97 +    val ctxt'' = ProofContext.init_global thy''
    1.98      val _ = print_step options "Compiling equations..."
    1.99      val compiled_terms =
   1.100        Output.cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ =>
   1.101          compile_preds options
   1.102 -          (#comp_modifiers (dest_steps steps)) thy'' all_vs param_vs preds moded_clauses)
   1.103 -    val _ = print_compiled_terms options thy'' compiled_terms
   1.104 +          (#comp_modifiers (dest_steps steps)) ctxt'' all_vs param_vs preds moded_clauses)
   1.105 +    val _ = print_compiled_terms options ctxt'' compiled_terms
   1.106      val _ = print_step options "Proving equations..."
   1.107      val result_thms =
   1.108        Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>

     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed May 19 18:24:06 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed May 19 18:24:07 2010 +0200
     2.3 @@ -216,12 +216,13 @@
     2.4      (*val _ = Predicate_Compile_Core.print_all_modes compilation thy4*)
     2.5      val _ = Output.tracing ("Preprocessing time: " ^ string_of_int (snd preproc_time))
     2.6      val _ = Output.tracing ("Core compilation time: " ^ string_of_int (snd core_comp_time))
     2.7 -    val modes = Predicate_Compile_Core.modes_of compilation thy4 full_constname
     2.8 +    val ctxt4 = ProofContext.init_global thy4
     2.9 +    val modes = Predicate_Compile_Core.modes_of compilation ctxt4 full_constname
    2.10      val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
    2.11      val prog =
    2.12        if member eq_mode modes output_mode then
    2.13          let
    2.14 -          val name = Predicate_Compile_Core.function_name_of compilation thy4
    2.15 +          val name = Predicate_Compile_Core.function_name_of compilation ctxt4
    2.16              full_constname output_mode
    2.17            val T = 
    2.18              case compilation of