src/HOL/Tools/specification_package.ML
changeset 18921 f47c46d7d654
parent 18799 f137c5e971f5
child 19414 a21431e996bf
--- a/src/HOL/Tools/specification_package.ML	Fri Feb 03 17:08:03 2006 +0100
+++ b/src/HOL/Tools/specification_package.ML	Fri Feb 03 23:12:28 2006 +0100
@@ -95,7 +95,7 @@
 
 fun collect_consts (        t $ u,tms) = collect_consts (u,collect_consts (t,tms))
   | collect_consts (   Abs(_,_,t),tms) = collect_consts (t,tms)
-  | collect_consts (tm as Const _,tms) = gen_ins (op aconv) (tm,tms)
+  | collect_consts (tm as Const _,tms) = insert (op aconv) tm tms
   | collect_consts (            _,tms) = tms
 
 (* Complementing Type.varify... *)