src/HOL/Tools/datatype_realizer.ML
changeset 21646 c07b5b0e8492
parent 20286 4cf8e86a2d29
child 22578 b0eb5652f210
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Dec 05 00:29:19 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Dec 05 00:30:38 2006 +0100
     1.3 @@ -128,7 +128,7 @@
     1.4            REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
     1.5              REPEAT (etac allE i) THEN atac i)) 1)]);
     1.6  
     1.7 -    val ind_name = Thm.name_of_thm induction;
     1.8 +    val ind_name = Thm.get_name induction;
     1.9      val vs = map (fn i => List.nth (pnames, i)) is;
    1.10      val (thm', thy') = thy
    1.11        |> Theory.absolute_path
    1.12 @@ -196,7 +196,7 @@
    1.13              [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
    1.14               resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
    1.15  
    1.16 -    val exh_name = Thm.name_of_thm exhaustion;
    1.17 +    val exh_name = Thm.get_name exhaustion;
    1.18      val (thm', thy') = thy
    1.19        |> Theory.absolute_path
    1.20        |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])