Quot/Examples/IntEx.thy
changeset 762 baac4639ecef
parent 758 3104d62e7a16
child 764 a603aa6c9d01
--- a/Quot/Examples/IntEx.thy	Sat Dec 19 22:09:57 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Sat Dec 19 22:21:51 2009 +0100
@@ -100,7 +100,7 @@
 where
  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
-ML {* print_qconstinfo @{context} *}
+ML {* Quotient_Info.print_qconstinfo @{context} *}
 
 lemma plus_sym_pre:
   shows "my_plus a b \<approx> my_plus b a"