src/Pure/Isar/element.ML
changeset 47815 43f677b3ae91
parent 47249 c0481c3c2a6c
child 49750 444cfaa331c9
     1.1 --- a/src/Pure/Isar/element.ML	Fri Apr 27 21:47:47 2012 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Fri Apr 27 22:47:30 2012 +0200
     1.3 @@ -485,16 +485,14 @@
     1.4    | init (Constrains _) = I
     1.5    | init (Assumes asms) = Context.map_proof (fn ctxt =>
     1.6        let
     1.7 -        val asms' =
     1.8 -          Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) asms;
     1.9 +        val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms;
    1.10          val (_, ctxt') = ctxt
    1.11            |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
    1.12            |> Proof_Context.add_assms_i Assumption.assume_export asms';
    1.13        in ctxt' end)
    1.14    | init (Defines defs) = Context.map_proof (fn ctxt =>
    1.15        let
    1.16 -        val defs' =
    1.17 -          Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) defs;
    1.18 +        val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
    1.19          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
    1.20              let val ((c, _), t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
    1.21              in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);