src/Pure/Isar/expression.ML
changeset 36610 bafd82950e24
parent 35845 e5980f0ad025
child 36674 d95f39448121
     1.1 --- a/src/Pure/Isar/expression.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -642,7 +642,7 @@
     1.4        |> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
     1.5        |> PureThy.add_defs false
     1.6          [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
     1.7 -    val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
     1.8 +    val defs_ctxt = ProofContext.init_global defs_thy |> Variable.declare_term head;
     1.9  
    1.10      val cert = Thm.cterm_of defs_thy;
    1.11  
    1.12 @@ -729,7 +729,7 @@
    1.13        error ("Duplicate definition of locale " ^ quote name);
    1.14  
    1.15      val ((fixed, deps, body_elems), (parms, ctxt')) =
    1.16 -      prep_decl raw_import I raw_body (ProofContext.init thy);
    1.17 +      prep_decl raw_import I raw_body (ProofContext.init_global thy);
    1.18      val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
    1.19  
    1.20      val predicate_binding =
    1.21 @@ -795,7 +795,7 @@
    1.22  fun gen_interpretation prep_expr parse_prop prep_attr
    1.23      expression equations theory =
    1.24    let
    1.25 -    val ((propss, deps, export), expr_ctxt) = ProofContext.init theory
    1.26 +    val ((propss, deps, export), expr_ctxt) = ProofContext.init_global theory
    1.27        |> prep_expr expression;
    1.28  
    1.29      val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
    1.30 @@ -809,7 +809,8 @@
    1.31          val eqn_attrss = map2 (fn attrs => fn eqn =>
    1.32            ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
    1.33          fun meta_rewrite thy =
    1.34 -          map (Local_Defs.meta_rewrite_rule (ProofContext.init thy) #> Drule.abs_def) o maps snd;
    1.35 +          map (Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) #> Drule.abs_def) o
    1.36 +            maps snd;
    1.37        in
    1.38          thy
    1.39          |> PureThy.note_thmss Thm.lemmaK eqn_attrss