src/HOL/Tools/datatype_realizer.ML
changeset 16123 1381e90c2694
parent 15574 b1d1b5bfc464
child 17521 0f1c48de39f5
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue May 31 11:53:13 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue May 31 11:53:14 2005 +0200
     1.3 @@ -128,14 +128,13 @@
     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 {path, ...} = Sign.rep_sg sg;
     1.8      val ind_name = Thm.name_of_thm induction;
     1.9      val vs = map (fn i => List.nth (pnames, i)) is;
    1.10      val (thy', thm') = thy
    1.11        |> Theory.absolute_path
    1.12        |> PureThy.store_thm
    1.13          ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
    1.14 -      |>> Theory.add_path (NameSpace.pack (getOpt (path,[])));
    1.15 +      |>> Theory.restore_naming thy;
    1.16  
    1.17      val ivs = Drule.vars_of_terms
    1.18        [Logic.varify (DatatypeProp.make_ind [descr] sorts)];
    1.19 @@ -200,12 +199,11 @@
    1.20              [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
    1.21               resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
    1.22  
    1.23 -    val {path, ...} = Sign.rep_sg sg;
    1.24      val exh_name = Thm.name_of_thm exhaustion;
    1.25      val (thy', thm') = thy
    1.26        |> Theory.absolute_path
    1.27        |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])
    1.28 -      |>> Theory.add_path (NameSpace.pack (getOpt (path,[])));
    1.29 +      |>> Theory.restore_naming thy;
    1.30  
    1.31      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    1.32      val prf = forall_intr_prf (y, forall_intr_prf (P,