src/Pure/Isar/expression.ML
changeset 42360 da8817d01e7c
parent 42359 6ca5407863ed
child 42375 774df7c59508
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Apr 16 15:25:25 2011 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Apr 16 15:47:52 2011 +0200
     1.3 @@ -185,7 +185,7 @@
     1.4      val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
     1.5      val inst = Symtab.make insts'';
     1.6    in
     1.7 -    (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
     1.8 +    (Element.inst_morphism (Proof_Context.theory_of ctxt) (instT, inst) $>
     1.9        Morphism.binding_morphism (Binding.prefix mandatory prfx), ctxt')
    1.10    end;
    1.11  
    1.12 @@ -198,15 +198,15 @@
    1.13    Element.map_ctxt
    1.14     {binding = I,
    1.15      typ = prep_typ ctxt,
    1.16 -    term = prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt),
    1.17 -    pattern = prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt),
    1.18 +    term = prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt),
    1.19 +    pattern = prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt),
    1.20      fact = I,
    1.21      attrib = I};
    1.22  
    1.23  fun parse_concl prep_term ctxt concl =
    1.24    (map o map) (fn (t, ps) =>
    1.25 -    (prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) t,
    1.26 -      map (prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt)) ps)) concl;
    1.27 +    (prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t,
    1.28 +      map (prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps)) concl;
    1.29  
    1.30  
    1.31  (** Simultaneous type inference: instantiations + elements + conclusion **)
    1.32 @@ -247,12 +247,12 @@
    1.33      fun prep (_, pats) (ctxt, t :: ts) =
    1.34        let val ctxt' = Variable.auto_fixes t ctxt
    1.35        in
    1.36 -        ((t, Syntax.check_props (ProofContext.set_mode ProofContext.mode_pattern ctxt') pats),
    1.37 +        ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats),
    1.38            (ctxt', ts))
    1.39        end;
    1.40      val (cs', (context', _)) = fold_map prep cs
    1.41        (context, Syntax.check_terms
    1.42 -        (ProofContext.set_mode ProofContext.mode_schematic context) (map fst cs));
    1.43 +        (Proof_Context.set_mode Proof_Context.mode_schematic context) (map fst cs));
    1.44    in (cs', context') end;
    1.45  
    1.46  in
    1.47 @@ -279,7 +279,7 @@
    1.48  
    1.49  fun declare_elem prep_vars (Fixes fixes) ctxt =
    1.50        let val (vars, _) = prep_vars fixes ctxt
    1.51 -      in ctxt |> ProofContext.add_fixes vars |> snd end
    1.52 +      in ctxt |> Proof_Context.add_fixes vars |> snd end
    1.53    | declare_elem prep_vars (Constrains csts) ctxt =
    1.54        ctxt |> prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) |> snd
    1.55    | declare_elem _ (Assumes _) ctxt = ctxt
    1.56 @@ -322,7 +322,7 @@
    1.57  
    1.58  fun finish_inst ctxt (loc, (prfx, inst)) =
    1.59    let
    1.60 -    val thy = ProofContext.theory_of ctxt;
    1.61 +    val thy = Proof_Context.theory_of ctxt;
    1.62      val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
    1.63      val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
    1.64    in (loc, morph) end;
    1.65 @@ -346,7 +346,7 @@
    1.66  fun prep_full_context_statement parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
    1.67      {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_concl ctxt1 =
    1.68    let
    1.69 -    val thy = ProofContext.theory_of ctxt1;
    1.70 +    val thy = Proof_Context.theory_of ctxt1;
    1.71  
    1.72      val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
    1.73  
    1.74 @@ -377,7 +377,7 @@
    1.75        in check_autofix insts elems concl ctxt end;
    1.76  
    1.77      val fors = prep_vars_inst fixed ctxt1 |> fst;
    1.78 -    val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
    1.79 +    val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd;
    1.80      val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
    1.81  
    1.82      val add_free = fold_aterms
    1.83 @@ -397,7 +397,7 @@
    1.84      (* Retrieve parameter types *)
    1.85      val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.name o #1) fixes)
    1.86        | _ => fn ps => ps) (Fixes fors :: elems') [];
    1.87 -    val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6;
    1.88 +    val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
    1.89      val parms = xs ~~ Ts;  (* params from expression and elements *)
    1.90  
    1.91      val Fixes fors' = finish_primitive parms I (Fixes fors);
    1.92 @@ -409,16 +409,16 @@
    1.93  in
    1.94  
    1.95  fun cert_full_context_statement x =
    1.96 -  prep_full_context_statement (K I) (K I) ProofContext.cert_vars
    1.97 -  make_inst ProofContext.cert_vars (K I) x;
    1.98 +  prep_full_context_statement (K I) (K I) Proof_Context.cert_vars
    1.99 +  make_inst Proof_Context.cert_vars (K I) x;
   1.100  
   1.101  fun cert_read_full_context_statement x =
   1.102 -  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
   1.103 -  make_inst ProofContext.cert_vars (K I) x;
   1.104 +  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
   1.105 +  make_inst Proof_Context.cert_vars (K I) x;
   1.106  
   1.107  fun read_full_context_statement x =
   1.108 -  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
   1.109 -  parse_inst ProofContext.read_vars intern x;
   1.110 +  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
   1.111 +  parse_inst Proof_Context.read_vars intern x;
   1.112  
   1.113  end;
   1.114  
   1.115 @@ -433,7 +433,7 @@
   1.116         prep {strict = true, do_close = false, fixed_frees = true}
   1.117          ([], []) I raw_elems raw_concl context;
   1.118       val (_, context') = context |>
   1.119 -       ProofContext.set_stmt true |>
   1.120 +       Proof_Context.set_stmt true |>
   1.121         fold_map activate elems;
   1.122    in (concl, context') end;
   1.123  
   1.124 @@ -448,7 +448,7 @@
   1.125  (* Locale declaration: import + elements *)
   1.126  
   1.127  fun fix_params params =
   1.128 -  ProofContext.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
   1.129 +  Proof_Context.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
   1.130  
   1.131  local
   1.132  
   1.133 @@ -462,7 +462,7 @@
   1.134        fix_params fixed |>
   1.135        fold (Context.proof_map o Locale.activate_facts NONE) deps;
   1.136      val (elems', _) = context' |>
   1.137 -      ProofContext.set_stmt true |>
   1.138 +      Proof_Context.set_stmt true |>
   1.139        fold_map activate elems;
   1.140    in ((fixed, deps, elems'), (parms, ctxt')) end;
   1.141  
   1.142 @@ -488,7 +488,7 @@
   1.143  
   1.144  fun prep_goal_expression prep expression context =
   1.145    let
   1.146 -    val thy = ProofContext.theory_of context;
   1.147 +    val thy = Proof_Context.theory_of context;
   1.148  
   1.149      val ((fixed, deps, _, _), _) =
   1.150        prep {strict = true, do_close = true, fixed_frees = true} expression I [] [] context;
   1.151 @@ -566,7 +566,7 @@
   1.152  
   1.153  fun eval_inst ctxt (loc, morph) text =
   1.154    let
   1.155 -    val thy = ProofContext.theory_of ctxt;
   1.156 +    val thy = Proof_Context.theory_of ctxt;
   1.157      val (asm, defs) = Locale.specification_of thy loc;
   1.158      val asm' = Option.map (Morphism.term morph) asm;
   1.159      val defs' = map (Morphism.term morph) defs;
   1.160 @@ -616,7 +616,7 @@
   1.161  fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args =>
   1.162    if length args = n then
   1.163      Syntax.const "_aprop" $   (* FIXME avoid old-style early externing (!??) *)
   1.164 -      Term.list_comb (Syntax.free (ProofContext.extern_const ctxt c), args)
   1.165 +      Term.list_comb (Syntax.free (Proof_Context.extern_const ctxt c), args)
   1.166    else raise Match);
   1.167  
   1.168  (* define one predicate including its intro rule and axioms
   1.169 @@ -651,7 +651,7 @@
   1.170        |> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
   1.171        |> Global_Theory.add_defs false
   1.172          [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
   1.173 -    val defs_ctxt = ProofContext.init_global defs_thy |> Variable.declare_term head;
   1.174 +    val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
   1.175  
   1.176      val cert = Thm.cterm_of defs_thy;
   1.177  
   1.178 @@ -738,7 +738,7 @@
   1.179        error ("Duplicate definition of locale " ^ quote name);
   1.180  
   1.181      val ((fixed, deps, body_elems), (parms, ctxt')) =
   1.182 -      prep_decl raw_import I raw_body (ProofContext.init_global thy);
   1.183 +      prep_decl raw_import I raw_body (Proof_Context.init_global thy);
   1.184      val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
   1.185  
   1.186      val extraTs =
   1.187 @@ -825,7 +825,7 @@
   1.188  fun gen_interpretation prep_expr parse_prop prep_attr
   1.189      expression equations theory =
   1.190    let
   1.191 -    val ((propss, deps, export), expr_ctxt) = ProofContext.init_global theory
   1.192 +    val ((propss, deps, export), expr_ctxt) = Proof_Context.init_global theory
   1.193        |> prep_expr expression;
   1.194  
   1.195      val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
   1.196 @@ -834,7 +834,7 @@
   1.197      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
   1.198  
   1.199      fun after_qed witss eqns =
   1.200 -      (ProofContext.background_theory o Context.theory_map)
   1.201 +      (Proof_Context.background_theory o Context.theory_map)
   1.202          (note_eqns_register deps witss attrss eqns export export');
   1.203  
   1.204    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
   1.205 @@ -844,7 +844,7 @@
   1.206    let
   1.207      val _ = Proof.assert_forward_or_chain state;
   1.208      val ctxt = Proof.context_of state;
   1.209 -    val theory = ProofContext.theory_of ctxt;
   1.210 +    val theory = Proof_Context.theory_of ctxt;
   1.211  
   1.212      val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
   1.213  
   1.214 @@ -891,7 +891,7 @@
   1.215    in
   1.216      ctxt
   1.217      |> Locale.add_thmss target Thm.lemmaK facts
   1.218 -    |> ProofContext.background_theory (fold (fn ((dep, morph), wits) =>
   1.219 +    |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
   1.220        fn theory =>
   1.221          Locale.add_dependency target
   1.222            (dep, morph $> Element.satisfy_morphism