src/Pure/Isar/element.ML
changeset 49750 444cfaa331c9
parent 47815 43f677b3ae91
child 52230 1105b3b5aa77
     1.1 --- a/src/Pure/Isar/element.ML	Tue Oct 09 20:23:58 2012 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Tue Oct 09 21:33:12 2012 +0200
     1.3 @@ -493,9 +493,9 @@
     1.4    | init (Defines defs) = Context.map_proof (fn ctxt =>
     1.5        let
     1.6          val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
     1.7 -        val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
     1.8 -            let val ((c, _), t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
     1.9 -            in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
    1.10 +        val asms = defs' |> map (fn (b, (t, ps)) =>
    1.11 +            let val (_, t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
    1.12 +            in (t', (b, [(t', ps)])) end);
    1.13          val (_, ctxt') = ctxt
    1.14            |> fold Variable.auto_fixes (map #1 asms)
    1.15            |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
    1.16 @@ -507,7 +507,13 @@
    1.17  
    1.18  fun activate_i elem ctxt =
    1.19    let
    1.20 -    val elem' = map_ctxt_attrib Args.assignable elem;
    1.21 +    val elem' =
    1.22 +      (case map_ctxt_attrib Args.assignable elem of
    1.23 +        Defines defs =>
    1.24 +          Defines (defs |> map (fn ((a, atts), (t, ps)) =>
    1.25 +            ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts),
    1.26 +              (t, ps))))
    1.27 +      | e => e);
    1.28      val ctxt' = Context.proof_map (init elem') ctxt;
    1.29    in (map_ctxt_attrib Args.closure elem', ctxt') end;
    1.30