src/Pure/Isar/expression.ML
changeset 54742 7a86358a3c0b
parent 54740 91f54d386680
child 54865 82bfac35f16f
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -619,7 +619,7 @@
     1.4      val bodyT = Term.fastype_of body;
     1.5    in
     1.6      if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
     1.7 -    else (body, bodyT, Object_Logic.atomize (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    end;
    1.10  
    1.11  (* achieve plain syntax for locale predicates (without "PROP") *)
    1.12 @@ -669,20 +669,22 @@
    1.13  
    1.14      val cert = Thm.cterm_of defs_thy;
    1.15  
    1.16 -    val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
    1.17 -      rewrite_goals_tac [pred_def] THEN
    1.18 -      compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
    1.19 -      compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
    1.20 +    val intro = Goal.prove_global defs_thy [] norm_ts statement
    1.21 +      (fn {context = ctxt, ...} =>
    1.22 +        rewrite_goals_tac ctxt [pred_def] THEN
    1.23 +        compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
    1.24 +        compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
    1.25  
    1.26      val conjuncts =
    1.27 -      (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
    1.28 +      (Drule.equal_elim_rule2 OF
    1.29 +        [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (cert statement))])
    1.30        |> Conjunction.elim_balanced (length ts);
    1.31  
    1.32      val (_, axioms_ctxt) = defs_ctxt
    1.33        |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
    1.34      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
    1.35        Element.prove_witness axioms_ctxt t
    1.36 -       (rewrite_goals_tac defs THEN compose_tac (false, ax, 0) 1));
    1.37 +       (rewrite_goals_tac axioms_ctxt defs THEN compose_tac (false, ax, 0) 1));
    1.38    in ((statement, intro, axioms), defs_thy) end;
    1.39  
    1.40  in
    1.41 @@ -849,7 +851,7 @@
    1.42      val dep_morphs = map2 (fn (dep, morph) => fn wits =>
    1.43        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
    1.44      fun activate' dep_morph ctxt = activate dep_morph
    1.45 -      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
    1.46 +        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
    1.47    in
    1.48      ctxt'
    1.49      |> fold activate' dep_morphs