src/Pure/Isar/code.ML
changeset 28703 aef727ef30e5
parent 28695 f7a06d7284c8
child 28708 a1a436f09ec6
     1.1 --- a/src/Pure/Isar/code.ML	Tue Oct 28 12:29:57 2008 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Tue Oct 28 16:58:59 2008 +0100
     1.3 @@ -11,7 +11,8 @@
     1.4    val add_eqn: thm -> theory -> theory
     1.5    val add_nonlinear_eqn: thm -> theory -> theory
     1.6    val add_default_eqn: thm -> theory -> theory
     1.7 -  val add_default_eqn_attr: Attrib.src
     1.8 +  val add_default_eqn_attribute: attribute
     1.9 +  val add_default_eqn_attrib: Attrib.src
    1.10    val del_eqn: thm -> theory -> theory
    1.11    val del_eqns: string -> theory -> theory
    1.12    val add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory
    1.13 @@ -571,8 +572,9 @@
    1.14        (fn thy => map (Code_Unit.assert_linear) o certify_const thy c) lthms;
    1.15    in change_eqns false c (add_lthms lthms') thy end;
    1.16  
    1.17 -val add_default_eqn_attr = Attrib.internal (fn _ => Thm.declaration_attribute
    1.18 -  (fn thm => Context.mapping (add_default_eqn thm) I));
    1.19 +val add_default_eqn_attribute = Thm.declaration_attribute
    1.20 +  (fn thm => Context.mapping (add_default_eqn thm) I);
    1.21 +val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
    1.22  
    1.23  fun del_eqn thm thy = case mk_syntactic_eqn thy thm
    1.24   of SOME (thm, _) => change_eqns true (Code_Unit.const_eqn thm) (del_thm thm) thy
    1.25 @@ -590,13 +592,9 @@
    1.26    let
    1.27      val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
    1.28      val (tyco, vs_cos) = Code_Unit.constrset_of_consts thy cs;
    1.29 -    val cs' = map fst (snd vs_cos);
    1.30 -    val purge_cs = case get_datatype thy tyco
    1.31 -     of (_, []) => NONE
    1.32 -      | (_, cos) => SOME (cs' @ map fst cos);
    1.33    in
    1.34      thy
    1.35 -    |> map_exec_purge purge_cs
    1.36 +    |> map_exec_purge NONE
    1.37          ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
    1.38          #> map_eqns (fold (Symtab.delete_safe o fst) cs))
    1.39      |> TypeInterpretation.data (tyco, serial ())