src/HOL/Tools/datatype_realizer.ML
changeset 24712 64ed05609568
parent 24711 e8bba7723858
child 25223 7463251e7273
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Sep 25 15:34:35 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Sep 25 17:06:14 2007 +0200
     1.3 @@ -130,10 +130,10 @@
     1.4      val ind_name = Thm.get_name induction;
     1.5      val vs = map (fn i => List.nth (pnames, i)) is;
     1.6      val (thm', thy') = thy
     1.7 -      |> Theory.absolute_path
     1.8 +      |> Sign.absolute_path
     1.9        |> PureThy.store_thm
    1.10          ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
    1.11 -      ||> Theory.restore_naming thy;
    1.12 +      ||> Sign.restore_naming thy;
    1.13  
    1.14      val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
    1.15      val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
    1.16 @@ -197,9 +197,9 @@
    1.17  
    1.18      val exh_name = Thm.get_name exhaustion;
    1.19      val (thm', thy') = thy
    1.20 -      |> Theory.absolute_path
    1.21 +      |> Sign.absolute_path
    1.22        |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])
    1.23 -      ||> Theory.restore_naming thy;
    1.24 +      ||> Sign.restore_naming thy;
    1.25  
    1.26      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    1.27      val prf = forall_intr_prf (y, forall_intr_prf (P,