src/HOL/Import/proof_kernel.ML
changeset 18728 6790126ab5f6
parent 18678 dd0c569fa43d
child 18929 d81435108688
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -1988,7 +1988,7 @@
     1.4  	    val thy1 = foldr (fn(name,thy)=>
     1.5  				snd (get_defname thyname name thy)) thy1 names
     1.6  	    fun new_name name = fst (get_defname thyname name thy1)
     1.7 -	    val (thy',res) = SpecificationPackage.add_specification_i NONE
     1.8 +	    val (thy',res) = SpecificationPackage.add_specification NONE
     1.9  				 (map (fn name => (new_name name,name,false)) names)
    1.10  				 (thy1,th)
    1.11  	    val res' = Drule.freeze_all res