src/HOL/Tools/res_clause.ML
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