src/ZF/Tools/induct_tacs.ML
changeset 6092 d9db67970c73
parent 6070 032babd0120b
child 6112 5e4871c5136b
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Tue Jan 12 13:40:08 1999 +0100
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Tue Jan 12 13:54:51 1999 +0100
     1.3 @@ -165,8 +165,7 @@
     1.4  
     1.5    in
     1.6        thy |> Theory.add_path (Sign.base_name big_rec_name)
     1.7 -	  |> PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), 
     1.8 -				  [Simplifier.simp_add_global])] 
     1.9 +	  |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
    1.10  	  |> DatatypesData.put 
    1.11  	      (Symtab.update
    1.12  	       ((big_rec_name, dt_info), DatatypesData.get thy))