changeset 18056 | 397b39b06ec8 |
parent 17999 | 6fe9cb1da9ed |
child 18199 | d236379ea408 |
1.1 --- a/src/HOL/Tools/res_clause.ML Wed Nov 02 14:46:47 2005 +0100 1.2 +++ b/src/HOL/Tools/res_clause.ML Wed Nov 02 14:46:49 2005 +0100 1.3 @@ -290,7 +290,7 @@ 1.4 1.5 (*Initialize the type suppression mechanism with the current theory before 1.6 producing any clauses!*) 1.7 -fun init thy = (monomorphic := Sign.monomorphic thy); 1.8 +fun init thy = (monomorphic := Sign.const_monomorphic thy); 1.9 1.10 1.11 (*Flatten a type to a string while accumulating sort constraints on the TFress and