src/Pure/Isar/expression.ML
changeset 59621 291934bac95e
parent 59616 eb59c6968219
child 59623 920889b0788e
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -629,8 +629,8 @@
     1.4      val bodyT = Term.fastype_of body;
     1.5    in
     1.6      if bodyT = propT
     1.7 -    then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
     1.8 -    else (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.cterm_of thy t))
     1.9 +    then (t, propT, Thm.reflexive (Thm.global_cterm_of thy t))
    1.10 +    else (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.global_cterm_of thy t))
    1.11    end;
    1.12  
    1.13  (* achieve plain syntax for locale predicates (without "PROP") *)
    1.14 @@ -684,11 +684,11 @@
    1.15          compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
    1.16          compose_tac defs_ctxt
    1.17            (false,
    1.18 -            Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_thy) norm_ts), 0) 1);
    1.19 +            Conjunction.intr_balanced (map (Thm.assume o Thm.global_cterm_of defs_thy) norm_ts), 0) 1);
    1.20  
    1.21      val conjuncts =
    1.22        (Drule.equal_elim_rule2 OF
    1.23 -        [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_thy statement))])
    1.24 +        [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.global_cterm_of defs_thy statement))])
    1.25        |> Conjunction.elim_balanced (length ts);
    1.26  
    1.27      val (_, axioms_ctxt) = defs_ctxt
    1.28 @@ -705,7 +705,7 @@
    1.29  fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy =
    1.30    let
    1.31      val ctxt = Proof_Context.init_global thy;
    1.32 -    val defs' = map (Thm.cterm_of thy #> Assumption.assume ctxt #> Drule.abs_def) defs;
    1.33 +    val defs' = map (Thm.global_cterm_of thy #> Assumption.assume ctxt #> Drule.abs_def) defs;
    1.34  
    1.35      val (a_pred, a_intro, a_axioms, thy'') =
    1.36        if null exts then (NONE, NONE, [], thy)
    1.37 @@ -757,7 +757,7 @@
    1.38  
    1.39  fun defines_to_notes ctxt (Defines defs) =
    1.40        Notes ("", map (fn (a, (def, _)) =>
    1.41 -        (a, [([Assumption.assume ctxt (Proof_Context.cterm_of ctxt def)],
    1.42 +        (a, [([Assumption.assume ctxt (Thm.cterm_of ctxt def)],
    1.43            [(Attrib.internal o K) Locale.witness_add])])) defs)
    1.44    | defines_to_notes _ e = e;
    1.45  
    1.46 @@ -806,7 +806,7 @@
    1.47      val notes =
    1.48        if is_some asm then
    1.49          [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
    1.50 -          [([Assumption.assume pred_ctxt (Thm.cterm_of thy' (the asm))],
    1.51 +          [([Assumption.assume pred_ctxt (Thm.global_cterm_of thy' (the asm))],
    1.52              [(Attrib.internal o K) Locale.witness_add])])])]
    1.53        else [];
    1.54