src/Pure/Isar/expression.ML
changeset 54883 dd04a8b654fc
parent 54879 a9397557da56
child 55639 e4e8cbd9d780
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Dec 31 11:19:14 2013 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Tue Dec 31 14:29:16 2013 +0100
     1.3 @@ -693,7 +693,8 @@
     1.4  
     1.5  fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy =
     1.6    let
     1.7 -    val defs' = map (cterm_of thy #> Assumption.assume #> Drule.abs_def) defs;
     1.8 +    val ctxt = Proof_Context.init_global thy;
     1.9 +    val defs' = map (cterm_of thy #> Assumption.assume ctxt #> Drule.abs_def) defs;
    1.10  
    1.11      val (a_pred, a_intro, a_axioms, thy'') =
    1.12        if null exts then (NONE, NONE, [], thy)
    1.13 @@ -717,13 +718,15 @@
    1.14            val ((statement, intro, axioms), thy''') =
    1.15              thy''
    1.16              |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
    1.17 +          val ctxt''' = Proof_Context.init_global thy''';
    1.18            val (_, thy'''') =
    1.19              thy'''
    1.20              |> Sign.qualified_path true binding
    1.21              |> Global_Theory.note_thmss ""
    1.22                   [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
    1.23                    ((Binding.conceal (Binding.name axiomsN), []),
    1.24 -                    [(map (Drule.export_without_context o Element.conclude_witness) axioms, [])])]
    1.25 +                    [(map (Drule.export_without_context o Element.conclude_witness ctxt''') axioms,
    1.26 +                      [])])]
    1.27              ||> Sign.restore_naming thy''';
    1.28          in (SOME statement, SOME intro, axioms, thy'''') end;
    1.29    in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
    1.30 @@ -740,9 +743,9 @@
    1.31        |> apfst (curry Notes "")
    1.32    | assumes_to_notes e axms = (e, axms);
    1.33  
    1.34 -fun defines_to_notes thy (Defines defs) =
    1.35 +fun defines_to_notes ctxt (Defines defs) =
    1.36        Notes ("", map (fn (a, (def, _)) =>
    1.37 -        (a, [([Assumption.assume (cterm_of thy def)],
    1.38 +        (a, [([Assumption.assume ctxt (cterm_of (Proof_Context.theory_of ctxt) def)],
    1.39            [(Attrib.internal o K) Locale.witness_add])])) defs)
    1.40    | defines_to_notes _ e = e;
    1.41  
    1.42 @@ -770,6 +773,7 @@
    1.43        else raw_predicate_binding;
    1.44      val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
    1.45        define_preds predicate_binding parms text thy;
    1.46 +    val pred_ctxt = Proof_Context.init_global thy';
    1.47  
    1.48      val a_satisfy = Element.satisfy_morphism a_axioms;
    1.49      val b_satisfy = Element.satisfy_morphism b_axioms;
    1.50 @@ -782,20 +786,21 @@
    1.51      val notes =
    1.52        if is_some asm then
    1.53          [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
    1.54 -          [([Assumption.assume (cterm_of thy' (the asm))],
    1.55 +          [([Assumption.assume pred_ctxt (cterm_of thy' (the asm))],
    1.56              [(Attrib.internal o K) Locale.witness_add])])])]
    1.57        else [];
    1.58  
    1.59      val notes' = body_elems |>
    1.60 -      map (defines_to_notes thy') |>
    1.61 +      map (defines_to_notes pred_ctxt) |>
    1.62        map (Element.transform_ctxt a_satisfy) |>
    1.63 -      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
    1.64 +      (fn elems =>
    1.65 +        fold_map assumes_to_notes elems (map (Element.conclude_witness pred_ctxt) a_axioms)) |>
    1.66        fst |>
    1.67        map (Element.transform_ctxt b_satisfy) |>
    1.68        map_filter (fn Notes notes => SOME notes | _ => NONE);
    1.69  
    1.70      val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
    1.71 -    val axioms = map Element.conclude_witness b_axioms;
    1.72 +    val axioms = map (Element.conclude_witness pred_ctxt) b_axioms;
    1.73  
    1.74      val loc_ctxt = thy'
    1.75        |> Locale.register_locale binding (extraTs, params)