clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional;
authorwenzelm
Tue Oct 09 20:05:17 2012 +0200 (2012-10-09)
changeset 49748a346daa8a1f4
parent 49747 2cf86639b77e
child 49749 f27c96e98672
clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional;
clarified Generic_Target.define: avoid duplicate def binding via Local_Defs.add_def;
src/Pure/Isar/local_defs.ML
src/Pure/Isar/proof.ML
src/Tools/induct.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Tue Oct 09 19:24:19 2012 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Oct 09 20:05:17 2012 +0200
     1.3 @@ -89,16 +89,14 @@
     1.4  fun add_defs defs ctxt =
     1.5    let
     1.6      val ((xs, mxs), specs) = defs |> split_list |>> split_list;
     1.7 -    val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
     1.8 -    val names = map2 Thm.def_binding_optional xs bfacts;
     1.9 +    val (bs, rhss) = specs |> split_list;
    1.10      val eqs = mk_def ctxt (xs ~~ rhss);
    1.11      val lhss = map (fst o Logic.dest_equals) eqs;
    1.12    in
    1.13      ctxt
    1.14      |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
    1.15      |> fold Variable.declare_term eqs
    1.16 -    |> Proof_Context.add_assms_i def_export
    1.17 -      (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
    1.18 +    |> Proof_Context.add_assms_i def_export (map2 (fn b => fn eq => (b, [(eq, [])])) bs eqs)
    1.19      |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
    1.20    end;
    1.21  
     2.1 --- a/src/Pure/Isar/proof.ML	Tue Oct 09 19:24:19 2012 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Tue Oct 09 20:05:17 2012 +0200
     2.3 @@ -643,7 +643,11 @@
     2.4      |>> map (fn (x, _, mx) => (x, mx))
     2.5      |-> (fn vars =>
     2.6        map_context_result (prep_binds false (map swap raw_rhss))
     2.7 -      #-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss)))))
     2.8 +      #-> (fn rhss =>
     2.9 +        let
    2.10 +          val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
    2.11 +            ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
    2.12 +        in map_context_result (Local_Defs.add_defs defs) end))
    2.13      |-> (set_facts o map (#2 o #2))
    2.14    end;
    2.15  
     3.1 --- a/src/Tools/induct.ML	Tue Oct 09 19:24:19 2012 +0200
     3.2 +++ b/src/Tools/induct.ML	Tue Oct 09 20:05:17 2012 +0200
     3.3 @@ -705,15 +705,15 @@
     3.4      fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
     3.5        | add (SOME (SOME x, (t, _))) ctxt =
     3.6            let val ([(lhs, (_, th))], ctxt') =
     3.7 -            Local_Defs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
     3.8 +            Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt
     3.9            in ((SOME lhs, [th]), ctxt') end
    3.10        | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
    3.11        | add (SOME (NONE, (t, _))) ctxt =
    3.12            let
    3.13              val (s, _) = Name.variant "x" (Variable.names_of ctxt);
    3.14 -            val ([(lhs, (_, th))], ctxt') =
    3.15 -              Local_Defs.add_defs [((Binding.name s, NoSyn),
    3.16 -                (Thm.empty_binding, t))] ctxt
    3.17 +            val x = Binding.name s;
    3.18 +            val ([(lhs, (_, th))], ctxt') = ctxt
    3.19 +              |> Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))];
    3.20            in ((SOME lhs, [th]), ctxt') end
    3.21        | add NONE ctxt = ((NONE, []), ctxt);
    3.22    in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;