src/HOL/Inductive.ML
changeset 3768 67f4ac759100
parent 2855 36f75c4a0047
child 4872 33e7cdc20681
     1.1 --- a/src/HOL/Inductive.ML	Wed Oct 01 17:43:42 1997 +0200
     1.2 +++ b/src/HOL/Inductive.ML	Wed Oct 01 18:13:41 1997 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4      val rec_tms = map (readtm sign termTVar) srec_tms
     1.5      and intr_tms = map (readtm sign propT) sintrs;
     1.6      val thy = thy |> Ind.add_fp_def_i(rec_tms, intr_tms) 
     1.7 -                  |> add_thyname thy_name);
     1.8 +                  |> Theory.add_name thy_name);
     1.9  
    1.10  
    1.11