src/HOL/Tools/datatype_codegen.ML
changeset 21046 fe1db2f991a7
parent 21012 f08574148b7a
child 21454 a1937c51ed88
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Mon Oct 16 14:07:21 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Mon Oct 16 14:07:31 2006 +0200
     1.3 @@ -490,30 +490,14 @@
     1.4  
     1.5  local
     1.6    val eq_def_sym = thm "eq_def" |> Thm.symmetric;
     1.7 -  val class_eq = "OperationalEquality.eq";
     1.8    fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
     1.9     of SOME _ => get_eq_datatype thy tyco
    1.10      | NONE => [TypecopyPackage.get_eq thy tyco];
    1.11 -  fun constrain_op_eq_thms thy thms =
    1.12 -    let
    1.13 -      fun add_eq (Const ("op =", ty)) =
    1.14 -            fold (insert (eq_fst (op =)))
    1.15 -              (Term.add_tvarsT ty [])
    1.16 -        | add_eq _ =
    1.17 -            I
    1.18 -      val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
    1.19 -      val instT = map (fn (v_i, sort) =>
    1.20 -        (Thm.ctyp_of thy (TVar (v_i, sort)),
    1.21 -           Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
    1.22 -    in
    1.23 -      thms
    1.24 -      |> map (Thm.instantiate (instT, []))
    1.25 -    end;
    1.26  in
    1.27    fun get_eq thy tyco =
    1.28      get_eq_thms thy tyco
    1.29      |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
    1.30 -    |> constrain_op_eq_thms thy
    1.31 +    |> HOL.constrain_op_eq_thms thy
    1.32      |> map (Tactic.rewrite_rule [eq_def_sym])
    1.33  end;
    1.34  
    1.35 @@ -615,15 +599,13 @@
    1.36  
    1.37  (* operational equality *)
    1.38  
    1.39 -local
    1.40 -  val class_eq = "OperationalEquality.eq";
    1.41 -in fun eq_hook specs =
    1.42 +fun eq_hook specs =
    1.43    let
    1.44      fun add_eq_thms (dtco, (_, (vs, cs))) thy =
    1.45        let
    1.46          val thy_ref = Theory.self_ref thy;
    1.47          val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
    1.48 -        val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
    1.49 +        val c = CodegenConsts.norm thy ("Code_Generator.eq", [ty]);
    1.50          val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
    1.51        in
    1.52          CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy
    1.53 @@ -631,9 +613,8 @@
    1.54    in
    1.55      prove_codetypes_arities (K (ClassPackage.intro_classes_tac []))
    1.56        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
    1.57 -      [class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
    1.58 +      [HOLogic.class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
    1.59    end;
    1.60 -end; (*local*)
    1.61  
    1.62  
    1.63