# HG changeset patch
# User wenzelm
# Date 1130939209 -3600
# Node ID 397b39b06ec8b33d1793a9266e78c505f3904ecb
# Parent  a93881a4422dc138ce6cdd90c7176a955088ee65
Sign.const_monomorphic;

diff -r a93881a4422d -r 397b39b06ec8 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Wed Nov 02 14:46:47 2005 +0100
+++ b/src/HOL/Tools/res_clause.ML	Wed Nov 02 14:46:49 2005 +0100
@@ -290,7 +290,7 @@
 
 (*Initialize the type suppression mechanism with the current theory before
     producing any clauses!*)
-fun init thy = (monomorphic := Sign.monomorphic thy);
+fun init thy = (monomorphic := Sign.const_monomorphic thy);
     
 
 (*Flatten a type to a string while accumulating sort constraints on the TFress and