moving towards working with proof contexts in the predicate compiler
authorbulwahn
Wed May 19 18:24:05 2010 +0200 (2010-05-19)
changeset 37003a393a588b82e
parent 37002 34e73e8bab66
child 37004 c62f743e37d4
moving towards working with proof contexts in the predicate compiler
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed May 19 18:24:04 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed May 19 18:24:05 2010 +0200
     1.3 @@ -74,7 +74,8 @@
     1.4    end
     1.5  
     1.6  fun preprocess_strong_conn_constnames options gr ts thy =
     1.7 -  if forall (fn (Const (c, _)) => Predicate_Compile_Core.is_registered thy c) ts then
     1.8 +  if forall (fn (Const (c, _)) =>
     1.9 +      Predicate_Compile_Core.is_registered (ProofContext.init_global thy) c) ts then
    1.10      thy
    1.11    else
    1.12      let
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:04 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:05 2010 +0200
     2.3 @@ -18,19 +18,21 @@
     2.4      -> ((string option * bool) * (compilation * int list)) -> int -> string -> Toplevel.state -> unit
     2.5    val register_predicate : (string * thm list * thm) -> theory -> theory
     2.6    val register_intros : string * thm list -> theory -> theory
     2.7 -  val is_registered : theory -> string -> bool
     2.8 -  val function_name_of : compilation -> theory -> string -> mode -> string
     2.9 +  val is_registered : Proof.context -> string -> bool
    2.10 +  val function_name_of : compilation -> Proof.context -> string -> mode -> string
    2.11    val predfun_intro_of: Proof.context -> string -> mode -> thm
    2.12    val predfun_elim_of: Proof.context -> string -> mode -> thm
    2.13 -  val all_preds_of : theory -> string list
    2.14 -  val modes_of: compilation -> theory -> string -> mode list
    2.15 -  val all_modes_of : compilation -> theory -> (string * mode list) list
    2.16 -  val all_random_modes_of : theory -> (string * mode list) list
    2.17 +  val all_preds_of : Proof.context -> string list
    2.18 +  val modes_of: compilation -> Proof.context -> string -> mode list
    2.19 +  val all_modes_of : compilation -> Proof.context -> (string * mode list) list
    2.20 +  val all_random_modes_of : Proof.context -> (string * mode list) list
    2.21    val intros_of : theory -> string -> thm list
    2.22    val add_intro : thm -> theory -> theory
    2.23    val set_elim : thm -> theory -> theory
    2.24    val register_alternative_function : string -> mode -> string -> theory -> theory
    2.25 -  val alternative_compilation_of : theory -> string -> mode ->
    2.26 +  val alternative_compilation_of_global : theory -> string -> mode ->
    2.27 +    (compilation_funs -> typ -> term) option
    2.28 +  val alternative_compilation_of : Proof.context -> string -> mode ->
    2.29      (compilation_funs -> typ -> term) option
    2.30    val functional_compilation : string -> mode -> compilation_funs -> typ -> term
    2.31    val force_modes_and_functions : string -> (mode * (string * bool)) list -> theory -> theory
    2.32 @@ -38,7 +40,7 @@
    2.33      (mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory
    2.34    val preprocess_intro : theory -> thm -> thm
    2.35    val print_stored_rules : theory -> unit
    2.36 -  val print_all_modes : compilation -> theory -> unit
    2.37 +  val print_all_modes : compilation -> Proof.context -> unit
    2.38    val mk_casesrule : Proof.context -> term -> thm list -> term
    2.39    val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
    2.40    val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int))
    2.41 @@ -235,9 +237,9 @@
    2.42   of NONE => error ("No such predicate " ^ quote name)  
    2.43    | SOME data => data;
    2.44  
    2.45 -val is_registered = is_some oo lookup_pred_data
    2.46 +val is_registered = is_some oo lookup_pred_data o ProofContext.theory_of
    2.47  
    2.48 -val all_preds_of = Graph.keys o PredData.get
    2.49 +val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of
    2.50  
    2.51  fun intros_of thy = map (Thm.transfer thy) o #intros o the_pred_data thy
    2.52  
    2.53 @@ -247,31 +249,34 @@
    2.54    
    2.55  val has_elim = is_some o #elim oo the_pred_data;
    2.56  
    2.57 -fun function_names_of compilation thy name =
    2.58 -  case AList.lookup (op =) (#function_names (the_pred_data thy name)) compilation of
    2.59 +fun function_names_of compilation ctxt name =
    2.60 +  case AList.lookup (op =) (#function_names (the_pred_data (ProofContext.theory_of ctxt) name)) compilation of
    2.61      NONE => error ("No " ^ string_of_compilation compilation
    2.62        ^ "functions defined for predicate " ^ quote name)
    2.63    | SOME fun_names => fun_names
    2.64  
    2.65 -fun function_name_of compilation thy name mode =
    2.66 +fun function_name_of compilation ctxt name mode =
    2.67    case AList.lookup eq_mode
    2.68 -    (function_names_of compilation thy name) mode of
    2.69 +    (function_names_of compilation ctxt name) mode of
    2.70      NONE => error ("No " ^ string_of_compilation compilation
    2.71        ^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
    2.72    | SOME function_name => function_name
    2.73  
    2.74 -fun modes_of compilation thy name = map fst (function_names_of compilation thy name)
    2.75 +fun modes_of compilation ctxt name = map fst (function_names_of compilation ctxt name)
    2.76  
    2.77 -fun all_modes_of compilation thy =
    2.78 -  map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
    2.79 -    (all_preds_of thy)
    2.80 +fun all_modes_of compilation ctxt =
    2.81 +  map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
    2.82 +    (all_preds_of ctxt)
    2.83  
    2.84  val all_random_modes_of = all_modes_of Random
    2.85  
    2.86 -fun defined_functions compilation thy name = case lookup_pred_data thy name of
    2.87 +fun defined_functions compilation ctxt name = case lookup_pred_data (ProofContext.theory_of ctxt) name of
    2.88      NONE => false
    2.89    | SOME data => AList.defined (op =) (#function_names data) compilation
    2.90  
    2.91 +fun needs_random ctxt s m =
    2.92 +  member (op =) (#needs_random (the_pred_data (ProofContext.theory_of ctxt) s)) m
    2.93 +
    2.94  fun lookup_predfun_data thy name mode =
    2.95    Option.map rep_predfun_data
    2.96      (AList.lookup (op =) (#predfun_data (the_pred_data thy name)) mode)
    2.97 @@ -308,18 +313,18 @@
    2.98      val _ = tracing (cat_lines (map print_pred pred_mode_table))
    2.99    in () end;
   2.100  
   2.101 -fun string_of_prem thy (Prem t) =
   2.102 -    (Syntax.string_of_term_global thy t) ^ "(premise)"
   2.103 -  | string_of_prem thy (Negprem t) =
   2.104 -    (Syntax.string_of_term_global thy (HOLogic.mk_not t)) ^ "(negative premise)"
   2.105 -  | string_of_prem thy (Sidecond t) =
   2.106 -    (Syntax.string_of_term_global thy t) ^ "(sidecondition)"
   2.107 -  | string_of_prem thy _ = raise Fail "string_of_prem: unexpected input"
   2.108 +fun string_of_prem ctxt (Prem t) =
   2.109 +    (Syntax.string_of_term ctxt t) ^ "(premise)"
   2.110 +  | string_of_prem ctxt (Negprem t) =
   2.111 +    (Syntax.string_of_term ctxt (HOLogic.mk_not t)) ^ "(negative premise)"
   2.112 +  | string_of_prem ctxt (Sidecond t) =
   2.113 +    (Syntax.string_of_term ctxt t) ^ "(sidecondition)"
   2.114 +  | string_of_prem ctxt _ = raise Fail "string_of_prem: unexpected input"
   2.115  
   2.116 -fun string_of_clause thy pred (ts, prems) =
   2.117 +fun string_of_clause ctxt pred (ts, prems) =
   2.118    (space_implode " --> "
   2.119 -  (map (string_of_prem thy) prems)) ^ " --> " ^ pred ^ " "
   2.120 -   ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))
   2.121 +  (map (string_of_prem ctxt) prems)) ^ " --> " ^ pred ^ " "
   2.122 +   ^ (space_implode " " (map (Syntax.string_of_term ctxt) ts))
   2.123  
   2.124  fun print_compiled_terms options thy =
   2.125    if show_compilation options then
   2.126 @@ -344,7 +349,7 @@
   2.127      fold print preds ()
   2.128    end;
   2.129  
   2.130 -fun print_all_modes compilation thy =
   2.131 +fun print_all_modes compilation ctxt =
   2.132    let
   2.133      val _ = writeln ("Inferred modes:")
   2.134      fun print (pred, modes) u =
   2.135 @@ -353,7 +358,7 @@
   2.136          val _ = writeln ("modes: " ^ (commas (map string_of_mode modes)))
   2.137        in u end
   2.138    in
   2.139 -    fold print (all_modes_of compilation thy) ()
   2.140 +    fold print (all_modes_of compilation ctxt) ()
   2.141    end
   2.142  
   2.143  (* validity checks *)
   2.144 @@ -576,12 +581,12 @@
   2.145        (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
   2.146      (Thm.transfer thy rule)
   2.147  
   2.148 -fun preprocess_elim thy elimrule =
   2.149 +fun preprocess_elim ctxt elimrule =
   2.150    let
   2.151      fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
   2.152         HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
   2.153       | replace_eqs t = t
   2.154 -    val ctxt = ProofContext.init_global thy
   2.155 +    val thy = ProofContext.theory_of ctxt
   2.156      val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt
   2.157      val prems = Thm.prems_of elimrule
   2.158      val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems))))
   2.159 @@ -636,16 +641,16 @@
   2.160      val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
   2.161    in PredData.map (Graph.map_node name (map_pred_data add)) end
   2.162  
   2.163 -fun is_inductive_predicate thy name =
   2.164 -  is_some (try (Inductive.the_inductive (ProofContext.init_global thy)) name)
   2.165 +fun is_inductive_predicate ctxt name =
   2.166 +  is_some (try (Inductive.the_inductive ctxt) name)
   2.167  
   2.168 -fun depending_preds_of thy (key, value) =
   2.169 +fun depending_preds_of ctxt (key, value) =
   2.170    let
   2.171      val intros = (#intros o rep_pred_data) value
   2.172    in
   2.173      fold Term.add_const_names (map Thm.prop_of intros) []
   2.174        |> filter (fn c => (not (c = key)) andalso
   2.175 -        (is_inductive_predicate thy c orelse is_registered thy c))
   2.176 +        (is_inductive_predicate ctxt c orelse is_registered ctxt c))
   2.177    end;
   2.178  
   2.179  fun add_intro thm thy =
   2.180 @@ -668,7 +673,7 @@
   2.181  fun register_predicate (constname, pre_intros, pre_elim) thy =
   2.182    let
   2.183      val intros = map (preprocess_intro thy) pre_intros
   2.184 -    val elim = preprocess_elim thy pre_elim
   2.185 +    val elim = preprocess_elim (ProofContext.init_global thy) pre_elim
   2.186    in
   2.187      if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
   2.188        PredData.map
   2.189 @@ -726,9 +731,13 @@
   2.190        (mode * (compilation_funs -> typ -> term)) list -> bool));
   2.191  );
   2.192  
   2.193 -fun alternative_compilation_of thy pred_name mode =
   2.194 +fun alternative_compilation_of_global thy pred_name mode =
   2.195    AList.lookup eq_mode (Symtab.lookup_list (Alt_Compilations_Data.get thy) pred_name) mode
   2.196  
   2.197 +fun alternative_compilation_of ctxt pred_name mode =
   2.198 +  AList.lookup eq_mode
   2.199 +    (Symtab.lookup_list (Alt_Compilations_Data.get (ProofContext.theory_of ctxt)) pred_name) mode
   2.200 +
   2.201  fun force_modes_and_compilations pred_name compilations =
   2.202    let
   2.203      (* thm refl is a dummy thm *)
   2.204 @@ -1158,10 +1167,10 @@
   2.205      in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
   2.206  *)
   2.207  
   2.208 -fun is_possible_output thy vs t =
   2.209 +fun is_possible_output ctxt vs t =
   2.210    forall
   2.211      (fn t => is_eqT (fastype_of t) andalso forall (member (op =) vs) (term_vs t))
   2.212 -      (non_invertible_subterms (ProofContext.init_global thy) t)
   2.213 +      (non_invertible_subterms ctxt t)
   2.214    andalso
   2.215      (forall (is_eqT o snd)
   2.216        (inter (fn ((f', _), f) => f = f') vs (Term.add_frees t [])))
   2.217 @@ -1177,7 +1186,7 @@
   2.218        []
   2.219    end
   2.220  
   2.221 -fun is_constructable thy vs t = forall (member (op =) vs) (term_vs t)
   2.222 +fun is_constructable vs t = forall (member (op =) vs) (term_vs t)
   2.223  
   2.224  fun missing_vars vs t = subtract (op =) vs (term_vs t)
   2.225  
   2.226 @@ -1197,11 +1206,11 @@
   2.227        SOME ms => SOME (map (fn m => (Context m , [])) ms)
   2.228      | NONE => NONE)
   2.229  
   2.230 -fun derivations_of (thy : theory) modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) =
   2.231 +fun derivations_of (ctxt : Proof.context) modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) =
   2.232      map_product
   2.233        (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
   2.234 -        (derivations_of thy modes vs t1 m1) (derivations_of thy modes vs t2 m2)
   2.235 -  | derivations_of thy modes vs t (m as Fun _) =
   2.236 +        (derivations_of ctxt modes vs t1 m1) (derivations_of ctxt modes vs t2 m2)
   2.237 +  | derivations_of ctxt modes vs t (m as Fun _) =
   2.238      (*let
   2.239        val (p, args) = strip_comb t
   2.240      in
   2.241 @@ -1217,37 +1226,37 @@
   2.242          end) ms
   2.243        | NONE => (if is_all_input mode then [(Context mode, [])] else []))
   2.244      end*)
   2.245 -    (case try (all_derivations_of thy modes vs) t  of
   2.246 +    (case try (all_derivations_of ctxt modes vs) t  of
   2.247        SOME derivs =>
   2.248          filter (fn (d, mvars) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs
   2.249      | NONE => (if is_all_input m then [(Context m, [])] else []))
   2.250 -  | derivations_of thy modes vs t m =
   2.251 +  | derivations_of ctxt modes vs t m =
   2.252      if eq_mode (m, Input) then
   2.253        [(Term Input, missing_vars vs t)]
   2.254      else if eq_mode (m, Output) then
   2.255 -      (if is_possible_output thy vs t then [(Term Output, [])] else [])
   2.256 +      (if is_possible_output ctxt vs t then [(Term Output, [])] else [])
   2.257      else []
   2.258 -and all_derivations_of thy modes vs (Const ("Pair", _) $ t1 $ t2) =
   2.259 +and all_derivations_of ctxt modes vs (Const ("Pair", _) $ t1 $ t2) =
   2.260    let
   2.261 -    val derivs1 = all_derivations_of thy modes vs t1
   2.262 -    val derivs2 = all_derivations_of thy modes vs t2
   2.263 +    val derivs1 = all_derivations_of ctxt modes vs t1
   2.264 +    val derivs2 = all_derivations_of ctxt modes vs t2
   2.265    in
   2.266      map_product
   2.267        (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
   2.268          derivs1 derivs2
   2.269    end
   2.270 -  | all_derivations_of thy modes vs (t1 $ t2) =
   2.271 +  | all_derivations_of ctxt modes vs (t1 $ t2) =
   2.272    let
   2.273 -    val derivs1 = all_derivations_of thy modes vs t1
   2.274 +    val derivs1 = all_derivations_of ctxt modes vs t1
   2.275    in
   2.276      maps (fn (d1, mvars1) =>
   2.277        case mode_of d1 of
   2.278          Fun (m', _) => map (fn (d2, mvars2) =>
   2.279 -          (Mode_App (d1, d2), union (op =) mvars1 mvars2)) (derivations_of thy modes vs t2 m')
   2.280 +          (Mode_App (d1, d2), union (op =) mvars1 mvars2)) (derivations_of ctxt modes vs t2 m')
   2.281          | _ => raise Fail "Something went wrong") derivs1
   2.282    end
   2.283 -  | all_derivations_of thy modes vs (Const (s, T)) = the (lookup_mode modes (Const (s, T)))
   2.284 -  | all_derivations_of thy modes vs (Free (x, T)) = the (lookup_mode modes (Free (x, T)))
   2.285 +  | all_derivations_of _ modes vs (Const (s, T)) = the (lookup_mode modes (Const (s, T)))
   2.286 +  | all_derivations_of _ modes vs (Free (x, T)) = the (lookup_mode modes (Free (x, T)))
   2.287    | all_derivations_of _ modes vs _ = raise Fail "all_derivations_of"
   2.288  
   2.289  fun rev_option_ord ord (NONE, NONE) = EQUAL
   2.290 @@ -1288,7 +1297,7 @@
   2.291        EQUAL => lexl_ord ords' (x, x')
   2.292      | ord => ord
   2.293  
   2.294 -fun deriv_ord' thy pol pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
   2.295 +fun deriv_ord' ctxt pol pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
   2.296    let
   2.297      (* prefer functional modes if it is a function *)
   2.298      fun fun_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   2.299 @@ -1296,7 +1305,7 @@
   2.300          fun is_functional t mode =
   2.301            case try (fst o dest_Const o fst o strip_comb) t of
   2.302              NONE => false
   2.303 -          | SOME c => is_some (alternative_compilation_of thy c mode)
   2.304 +          | SOME c => is_some (alternative_compilation_of ctxt c mode)
   2.305        in
   2.306          case (is_functional t1 (head_mode_of deriv1), is_functional t2 (head_mode_of deriv2)) of
   2.307            (true, true) => EQUAL
   2.308 @@ -1326,7 +1335,7 @@
   2.309      ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2))
   2.310    end
   2.311  
   2.312 -fun deriv_ord thy pol pred modes t = deriv_ord' thy pol pred modes t t
   2.313 +fun deriv_ord ctxt pol pred modes t = deriv_ord' ctxt pol pred modes t t
   2.314  
   2.315  fun premise_ord thy pol pred modes ((prem1, a1), (prem2, a2)) =
   2.316    rev_option_ord (deriv_ord' thy pol pred modes (dest_indprem prem1) (dest_indprem prem2)) (a1, a2)
   2.317 @@ -1335,25 +1344,25 @@
   2.318    tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^
   2.319      commas (map (fn (m, r) => string_of_mode m ^ (if r then " random " else " not ")) ms)) modes)))
   2.320  
   2.321 -fun select_mode_prem (mode_analysis_options : mode_analysis_options) (thy : theory) pred
   2.322 +fun select_mode_prem (mode_analysis_options : mode_analysis_options) (ctxt : Proof.context) pred
   2.323    pol (modes, (pos_modes, neg_modes)) vs ps =
   2.324    let
   2.325      fun choose_mode_of_prem (Prem t) = partial_hd
   2.326 -        (sort (deriv_ord thy pol pred modes t) (all_derivations_of thy pos_modes vs t))
   2.327 +        (sort (deriv_ord ctxt pol pred modes t) (all_derivations_of ctxt pos_modes vs t))
   2.328        | choose_mode_of_prem (Sidecond t) = SOME (Context Bool, missing_vars vs t)
   2.329        | choose_mode_of_prem (Negprem t) = partial_hd
   2.330 -          (sort (deriv_ord thy (not pol) pred modes t)
   2.331 +          (sort (deriv_ord ctxt (not pol) pred modes t)
   2.332            (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
   2.333 -             (all_derivations_of thy neg_modes vs t)))
   2.334 -      | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: " ^ string_of_prem thy p)
   2.335 +             (all_derivations_of ctxt neg_modes vs t)))
   2.336 +      | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: " ^ string_of_prem ctxt p)
   2.337    in
   2.338      if #reorder_premises mode_analysis_options then
   2.339 -      partial_hd (sort (premise_ord thy pol pred modes) (ps ~~ map choose_mode_of_prem ps))
   2.340 +      partial_hd (sort (premise_ord ctxt pol pred modes) (ps ~~ map choose_mode_of_prem ps))
   2.341      else
   2.342        SOME (hd ps, choose_mode_of_prem (hd ps))
   2.343    end
   2.344  
   2.345 -fun check_mode_clause' (mode_analysis_options : mode_analysis_options) thy pred param_vs (modes :
   2.346 +fun check_mode_clause' (mode_analysis_options : mode_analysis_options) ctxt pred param_vs (modes :
   2.347    (string * ((bool * mode) * bool) list) list) ((pol, mode) : bool * mode) (ts, ps) =
   2.348    let
   2.349      val vTs = distinct (op =) (fold Term.add_frees (map dest_indprem ps) (fold Term.add_frees ts []))
   2.350 @@ -1368,7 +1377,7 @@
   2.351            val modes = map (fn (s, ms) => (s, map (fn ((p, m), r) => m) ms)) modes'
   2.352          in (modes, modes) end
   2.353      val (in_ts, out_ts) = split_mode mode ts
   2.354 -    val in_vs = maps (vars_of_destructable_term (ProofContext.init_global thy)) in_ts
   2.355 +    val in_vs = maps (vars_of_destructable_term ctxt) in_ts
   2.356      val out_vs = terms_vs out_ts
   2.357      fun known_vs_after p vs = (case p of
   2.358          Prem t => union (op =) vs (term_vs t)
   2.359 @@ -1378,7 +1387,7 @@
   2.360      fun check_mode_prems acc_ps rnd vs [] = SOME (acc_ps, vs, rnd)
   2.361        | check_mode_prems acc_ps rnd vs ps =
   2.362          (case
   2.363 -          (select_mode_prem mode_analysis_options thy pred pol (modes', (pos_modes', neg_modes')) vs ps) of
   2.364 +          (select_mode_prem mode_analysis_options ctxt pred pol (modes', (pos_modes', neg_modes')) vs ps) of
   2.365            SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd
   2.366              (known_vs_after p vs) (filter_out (equal p) ps)
   2.367          | SOME (p, SOME (deriv, missing_vars)) =>
   2.368 @@ -1394,7 +1403,7 @@
   2.369      case check_mode_prems [] false in_vs ps of
   2.370        NONE => NONE
   2.371      | SOME (acc_ps, vs, rnd) =>
   2.372 -      if forall (is_constructable thy vs) (in_ts @ out_ts) then
   2.373 +      if forall (is_constructable vs) (in_ts @ out_ts) then
   2.374          SOME (ts, rev acc_ps, rnd)
   2.375        else
   2.376          if #use_random mode_analysis_options andalso pol then
   2.377 @@ -1474,11 +1483,12 @@
   2.378  
   2.379  fun infer_modes mode_analysis_options options compilation preds all_modes param_vs clauses thy =
   2.380    let
   2.381 +    val ctxt = ProofContext.init_global thy  
   2.382      val collect_errors = false
   2.383      fun appair f (x1, x2) (y1, y2) = (f x1 y1, f x2 y2)
   2.384 -    fun needs_random s (false, m) = ((false, m), false)
   2.385 -      | needs_random s (true, m) = ((true, m), member (op =) (#needs_random (the_pred_data thy s)) m)
   2.386 -    fun add_polarity_and_random_bit s b ms = map (fn m => needs_random s (b, m)) ms
   2.387 +    fun add_needs_random s (false, m) = ((false, m), false)
   2.388 +      | add_needs_random s (true, m) = ((true, m), needs_random ctxt s m)
   2.389 +    fun add_polarity_and_random_bit s b ms = map (fn m => add_needs_random s (b, m)) ms
   2.390      val prednames = map fst preds
   2.391      (* extramodes contains all modes of all constants, should we only use the necessary ones
   2.392         - what is the impact on performance? *)
   2.393 @@ -1493,15 +1503,13 @@
   2.394        if #infer_pos_and_neg_modes mode_analysis_options then
   2.395          let
   2.396            val pos_extra_modes =
   2.397 -            map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
   2.398 +            map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
   2.399              relevant_prednames
   2.400 -            (* all_modes_of compilation thy *)
   2.401              |> filter_out (fn (name, _) => member (op =) prednames name)
   2.402            val neg_extra_modes =
   2.403            map_filter (fn name => Option.map (pair name)
   2.404 -            (try (modes_of (negative_compilation_of compilation) thy) name))
   2.405 +            (try (modes_of (negative_compilation_of compilation) ctxt) name))
   2.406              relevant_prednames
   2.407 -          (*all_modes_of (negative_compilation_of compilation) thy*)
   2.408              |> filter_out (fn (name, _) => member (op =) prednames name)
   2.409          in
   2.410            map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)
   2.411 @@ -1510,9 +1518,8 @@
   2.412          end
   2.413        else
   2.414          map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)))
   2.415 -          (map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
   2.416 +          (map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
   2.417              relevant_prednames
   2.418 -          (*all_modes_of compilation thy*)
   2.419            |> filter_out (fn (name, _) => member (op =) prednames name))
   2.420      val _ = print_extra_modes options extra_modes
   2.421      val start_modes =
   2.422 @@ -1522,7 +1529,7 @@
   2.423        else
   2.424          map (fn (s, ms) => (s, map (fn m => ((true, m), false)) ms)) all_modes
   2.425      fun iteration modes = map
   2.426 -      (check_modes_pred' mode_analysis_options options thy param_vs clauses
   2.427 +      (check_modes_pred' mode_analysis_options options ctxt param_vs clauses
   2.428          (modes @ extra_modes)) modes
   2.429      val ((modes : (string * ((bool * mode) * bool) list) list), errors) =
   2.430        Output.cond_timeit false "Fixpount computation of mode analysis" (fn () =>
   2.431 @@ -1533,7 +1540,7 @@
   2.432            in (modes', errors @ flat new_errors) end) (start_modes, [])
   2.433          else
   2.434            (fixp (fn modes => map fst (iteration modes)) start_modes, []))
   2.435 -    val moded_clauses = map (get_modes_pred' mode_analysis_options thy param_vs clauses
   2.436 +    val moded_clauses = map (get_modes_pred' mode_analysis_options ctxt param_vs clauses
   2.437        (modes @ extra_modes)) modes
   2.438      val thy' = fold (fn (s, ms) => if member (op =) (map fst preds) s then
   2.439        set_needs_random s (map_filter (fn ((true, m), true) => SOME m | _ => NONE) ms) else I)
   2.440 @@ -1672,11 +1679,11 @@
   2.441          (t, Term Input) => SOME t
   2.442        | (t, Term Output) => NONE
   2.443        | (Const (name, T), Context mode) =>
   2.444 -        (case alternative_compilation_of (ProofContext.theory_of ctxt) name mode of
   2.445 +        (case alternative_compilation_of ctxt name mode of
   2.446            SOME alt_comp => SOME (alt_comp compfuns T)
   2.447          | NONE =>
   2.448            SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
   2.449 -            (ProofContext.theory_of ctxt) name mode,
   2.450 +            ctxt name mode,
   2.451              Comp_Mod.funT_of compilation_modifiers mode T)))
   2.452        | (Free (s, T), Context m) =>
   2.453          SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
   2.454 @@ -1984,7 +1991,7 @@
   2.455          end
   2.456      val fun_const =
   2.457        Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
   2.458 -      (ProofContext.theory_of ctxt) s mode, funT)
   2.459 +      ctxt s mode, funT)
   2.460    in
   2.461      HOLogic.mk_Trueprop
   2.462        (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
   2.463 @@ -2045,7 +2052,7 @@
   2.464        (Free (x, T), x :: names)
   2.465      end
   2.466  
   2.467 -fun create_intro_elim_rule mode defthm mode_id funT pred thy =
   2.468 +fun create_intro_elim_rule ctxt mode defthm mode_id funT pred =
   2.469    let
   2.470      val funtrm = Const (mode_id, funT)
   2.471      val Ts = binder_types (fastype_of pred)
   2.472 @@ -2073,11 +2080,11 @@
   2.473      val simprules = [defthm, @{thm eval_pred},
   2.474        @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
   2.475      val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
   2.476 -    val introthm = Goal.prove (ProofContext.init_global thy)
   2.477 +    val introthm = Goal.prove ctxt
   2.478        (argnames @ hoarg_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac)
   2.479      val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
   2.480      val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
   2.481 -    val elimthm = Goal.prove (ProofContext.init_global thy)
   2.482 +    val elimthm = Goal.prove ctxt
   2.483        (argnames @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac)
   2.484      val opt_neg_introthm =
   2.485        if is_all_input mode then
   2.486 @@ -2091,7 +2098,7 @@
   2.487              Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps
   2.488                (@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1
   2.489              THEN rtac @{thm Predicate.singleI} 1
   2.490 -        in SOME (Goal.prove (ProofContext.init_global thy) (argnames @ hoarg_names') []
   2.491 +        in SOME (Goal.prove ctxt (argnames @ hoarg_names') []
   2.492              neg_introtrm (fn _ => tac))
   2.493          end
   2.494        else NONE
   2.495 @@ -2132,8 +2139,9 @@
   2.496          val ([definition], thy') = thy |>
   2.497            Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
   2.498            PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
   2.499 +        val ctxt' = ProofContext.init_global thy'
   2.500          val rules as ((intro, elim), _) =
   2.501 -          create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
   2.502 +          create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
   2.503          in thy'
   2.504            |> set_function_name Pred name mode mode_cname
   2.505            |> add_predfun_data name mode (definition, rules)
   2.506 @@ -2302,10 +2310,9 @@
   2.507  
   2.508  fun prove_sidecond ctxt t =
   2.509    let
   2.510 -    val thy = ProofContext.theory_of ctxt
   2.511      fun preds_of t nameTs = case strip_comb t of 
   2.512        (f as Const (name, T), args) =>
   2.513 -        if is_registered thy name then (name, T) :: nameTs
   2.514 +        if is_registered ctxt name then (name, T) :: nameTs
   2.515            else fold preds_of args nameTs
   2.516        | _ => nameTs
   2.517      val preds = preds_of t []
   2.518 @@ -2496,7 +2503,7 @@
   2.519  fun prove_sidecond2 options ctxt t = let
   2.520    fun preds_of t nameTs = case strip_comb t of 
   2.521      (f as Const (name, T), args) =>
   2.522 -      if is_registered (ProofContext.theory_of ctxt) name then (name, T) :: nameTs
   2.523 +      if is_registered ctxt name then (name, T) :: nameTs
   2.524          else fold preds_of args nameTs
   2.525      | _ => nameTs
   2.526    val preds = preds_of t []
   2.527 @@ -2650,25 +2657,25 @@
   2.528      compiled_terms
   2.529  
   2.530  (* preparation of introduction rules into special datastructures *)
   2.531 -fun dest_prem thy params t =
   2.532 +fun dest_prem ctxt params t =
   2.533    (case strip_comb t of
   2.534      (v as Free _, ts) => if member (op =) params v then Prem t else Sidecond t
   2.535 -  | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem thy params t of
   2.536 +  | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem ctxt params t of
   2.537        Prem t => Negprem t
   2.538      | Negprem _ => error ("Double negation not allowed in premise: " ^
   2.539 -        Syntax.string_of_term_global thy (c $ t)) 
   2.540 +        Syntax.string_of_term ctxt (c $ t)) 
   2.541      | Sidecond t => Sidecond (c $ t))
   2.542    | (c as Const (s, _), ts) =>
   2.543 -    if is_registered thy s then Prem t else Sidecond t
   2.544 +    if is_registered ctxt s then Prem t else Sidecond t
   2.545    | _ => Sidecond t)
   2.546  
   2.547  fun prepare_intrs options compilation thy prednames intros =
   2.548    let
   2.549 +    val ctxt = ProofContext.init_global thy
   2.550      val intrs = map prop_of intros
   2.551      val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames
   2.552      val (preds, intrs) = unify_consts thy preds intrs
   2.553 -    val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs]
   2.554 -      (ProofContext.init_global thy)
   2.555 +    val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs] ctxt
   2.556      val preds = map dest_Const preds
   2.557      val all_vs = terms_vs intrs
   2.558      val all_modes = 
   2.559 @@ -2699,7 +2706,7 @@
   2.560      fun add_clause intr clauses =
   2.561        let
   2.562          val (Const (name, T), ts) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
   2.563 -        val prems = map (dest_prem thy params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr)
   2.564 +        val prems = map (dest_prem ctxt params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr)
   2.565        in
   2.566          AList.update op = (name, these (AList.lookup op = clauses name) @
   2.567            [(ts, prems)]) clauses
   2.568 @@ -2763,13 +2770,13 @@
   2.569        let
   2.570          val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool
   2.571        in
   2.572 -        if member (op =) (modes_of Pred thy predname) full_mode then
   2.573 +        if member (op =) (modes_of Pred ctxt predname) full_mode then
   2.574            let
   2.575              val Ts = binder_types T
   2.576              val arg_names = Name.variant_list []
   2.577                (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
   2.578              val args = map2 (curry Free) arg_names Ts
   2.579 -            val predfun = Const (function_name_of Pred thy predname full_mode,
   2.580 +            val predfun = Const (function_name_of Pred ctxt predname full_mode,
   2.581                Ts ---> PredicateCompFuns.mk_predT @{typ unit})
   2.582              val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
   2.583              val eq_term = HOLogic.mk_Trueprop
   2.584 @@ -2874,8 +2881,9 @@
   2.585    let
   2.586      fun dest_steps (Steps s) = s
   2.587      val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps)))
   2.588 +    val ctxt = ProofContext.init_global thy
   2.589      val thy' = thy
   2.590 -      |> PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names)
   2.591 +      |> PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of ctxt)) names)
   2.592        |> Theory.checkpoint;
   2.593      fun strong_conn_of gr keys =
   2.594        Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
   2.595 @@ -2883,7 +2891,7 @@
   2.596      
   2.597      val thy'' = fold_rev
   2.598        (fn preds => fn thy =>
   2.599 -        if not (forall (defined thy) preds) then
   2.600 +        if not (forall (defined (ProofContext.init_global thy)) preds) then
   2.601            let
   2.602              val mode_analysis_options = {use_random = #use_random (dest_steps steps),
   2.603                reorder_premises =
   2.604 @@ -3026,8 +3034,9 @@
   2.605    let
   2.606      val thy = ProofContext.theory_of lthy
   2.607      val const = prep_const thy raw_const
   2.608 +    val ctxt = ProofContext.init_global thy
   2.609      val lthy' = Local_Theory.theory (PredData.map
   2.610 -        (extend (fetch_pred_data thy) (depending_preds_of thy) const)) lthy
   2.611 +        (extend (fetch_pred_data thy) (depending_preds_of ctxt) const)) lthy
   2.612      val thy' = ProofContext.theory_of lthy'
   2.613      val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim thy')
   2.614      fun mk_cases const =
   2.615 @@ -3084,11 +3093,11 @@
   2.616        (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) option)
   2.617  
   2.618  (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
   2.619 -fun analyze_compr thy compfuns param_user_modes (compilation, arguments) t_compr =
   2.620 +fun analyze_compr ctxt compfuns param_user_modes (compilation, arguments) t_compr =
   2.621    let
   2.622      val all_modes_of = all_modes_of compilation
   2.623      val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
   2.624 -      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
   2.625 +      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
   2.626      val (body, Ts, fp) = HOLogic.strip_psplits split;
   2.627      val output_names = Name.variant_list (Term.add_free_names body [])
   2.628        (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
   2.629 @@ -3099,9 +3108,9 @@
   2.630      val (pred as Const (name, T), all_args) =
   2.631        case strip_comb body of
   2.632          (Const (name, T), all_args) => (Const (name, T), all_args)
   2.633 -      | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term_global thy head)
   2.634 +      | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)
   2.635    in
   2.636 -    if defined_functions compilation thy name then
   2.637 +    if defined_functions compilation ctxt name then
   2.638        let
   2.639          fun extract_mode (Const ("Pair", _) $ t1 $ t2) = Pair (extract_mode t1, extract_mode t2)
   2.640            | extract_mode (Free (x, _)) = if member (op =) output_names x then Output else Input
   2.641 @@ -3130,7 +3139,7 @@
   2.642                    instance_of (Output, m1) andalso instance_of (Output, m2)
   2.643                | instance_of _ = false
   2.644            in forall instance_of (strip_fun_mode m1 ~~ strip_fun_mode m2) end
   2.645 -        val derivs = all_derivations_of thy (all_modes_of thy) [] body
   2.646 +        val derivs = all_derivations_of ctxt (all_modes_of ctxt) [] body
   2.647            |> filter (fn (d, missing_vars) =>
   2.648              let
   2.649                val (p_mode :: modes) = collect_context_modes d
   2.650 @@ -3142,10 +3151,10 @@
   2.651            |> map fst
   2.652          val deriv = case derivs of
   2.653              [] => error ("No mode possible for comprehension "
   2.654 -                    ^ Syntax.string_of_term_global thy t_compr)
   2.655 +                    ^ Syntax.string_of_term ctxt t_compr)
   2.656            | [d] => d
   2.657            | d :: _ :: _ => (warning ("Multiple modes possible for comprehension "
   2.658 -                    ^ Syntax.string_of_term_global thy t_compr); d);
   2.659 +                    ^ Syntax.string_of_term ctxt t_compr); d);
   2.660          val (_, outargs) = split_mode (head_mode_of deriv) all_args
   2.661          val additional_arguments =
   2.662            case compilation of
   2.663 @@ -3169,7 +3178,7 @@
   2.664            | DSeq => dseq_comp_modifiers
   2.665            | Pos_Random_DSeq => pos_random_dseq_comp_modifiers
   2.666            | New_Pos_Random_DSeq => new_pos_random_dseq_comp_modifiers
   2.667 -        val t_pred = compile_expr comp_modifiers (ProofContext.init_global thy)
   2.668 +        val t_pred = compile_expr comp_modifiers ctxt
   2.669            (body, deriv) additional_arguments;
   2.670          val T_pred = dest_predT compfuns (fastype_of t_pred)
   2.671          val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
   2.672 @@ -3180,7 +3189,7 @@
   2.673        error "Evaluation with values is not possible because compilation with code_pred was not invoked"
   2.674    end
   2.675  
   2.676 -fun eval thy stats param_user_modes (options as (compilation, arguments)) k t_compr =
   2.677 +fun eval ctxt stats param_user_modes (options as (compilation, arguments)) k t_compr =
   2.678    let
   2.679      fun count xs x =
   2.680        let
   2.681 @@ -3195,7 +3204,7 @@
   2.682        | Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns
   2.683        | New_Pos_Random_DSeq => New_Pos_Random_Sequence_CompFuns.compfuns
   2.684        | _ => PredicateCompFuns.compfuns
   2.685 -    val t = analyze_compr thy compfuns param_user_modes options t_compr;
   2.686 +    val t = analyze_compr ctxt compfuns param_user_modes options t_compr;
   2.687      val T = dest_predT compfuns (fastype_of t);
   2.688      val t' =
   2.689        if stats andalso compilation = New_Pos_Random_DSeq then
   2.690 @@ -3204,6 +3213,7 @@
   2.691              @{term Code_Numeral.of_nat} $ (HOLogic.size_const T $ Bound 0)))) t
   2.692        else
   2.693          mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
   2.694 +    val thy = ProofContext.theory_of ctxt
   2.695      val (ts, statistics) =
   2.696        case compilation of
   2.697         (* Random =>
   2.698 @@ -3255,8 +3265,7 @@
   2.699  
   2.700  fun values ctxt param_user_modes ((raw_expected, stats), comp_options) k t_compr =
   2.701    let
   2.702 -    val thy = ProofContext.theory_of ctxt
   2.703 -    val ((T, ts), statistics) = eval thy stats param_user_modes comp_options k t_compr
   2.704 +    val ((T, ts), statistics) = eval ctxt stats param_user_modes comp_options k t_compr
   2.705      val setT = HOLogic.mk_setT T
   2.706      val elems = HOLogic.mk_set T ts
   2.707      val cont = Free ("...", setT)