src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 32124 954321008785
parent 31902 862ae16a799d
child 32729 1441cf4ddc1a
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Jul 21 15:44:31 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Jul 21 15:52:30 2009 +0200
     1.3 @@ -93,7 +93,7 @@
     1.4      val _ = message config "Constructing primrec combinators ...";
     1.5  
     1.6      val big_name = space_implode "_" new_type_names;
     1.7 -    val thy0 = add_path (#flat_names config) big_name thy;
     1.8 +    val thy0 = Sign.add_path big_name thy;
     1.9  
    1.10      val descr' = List.concat descr;
    1.11      val recTs = get_rec_types descr' sorts;
    1.12 @@ -243,7 +243,7 @@
    1.13             Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    1.14               set $ Free ("x", T) $ Free ("y", T'))))))
    1.15                 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
    1.16 -      ||> parent_path (#flat_names config) 
    1.17 +      ||> Sign.parent_path
    1.18        ||> Theory.checkpoint;
    1.19  
    1.20  
    1.21 @@ -277,7 +277,7 @@
    1.22    let
    1.23      val _ = message config "Proving characteristic theorems for case combinators ...";
    1.24  
    1.25 -    val thy1 = add_path (#flat_names config) (space_implode "_" new_type_names) thy;
    1.26 +    val thy1 = Sign.add_path (space_implode "_" new_type_names) thy;
    1.27  
    1.28      val descr' = List.concat descr;
    1.29      val recTs = get_rec_types descr' sorts;
    1.30 @@ -339,7 +339,7 @@
    1.31      thy2
    1.32      |> Context.the_theory o fold (fold Nitpick_Const_Simps.add_thm) case_thms
    1.33         o Context.Theory
    1.34 -    |> parent_path (#flat_names config)
    1.35 +    |> Sign.parent_path
    1.36      |> store_thmss "cases" new_type_names case_thms
    1.37      |-> (fn thmss => pair (thmss, case_names))
    1.38    end;