# HG changeset patch
# User haftmann
# Date 1190299053 -7200
# Node ID a705b98345900535fb21a68849616bea23a7ec55
# Parent  8f94b16783f70d35db149a877552bb94b090d0bf
fixed cg setup

diff -r 8f94b16783f7 -r a705b9834590 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Thu Sep 20 16:37:32 2007 +0200
+++ b/src/HOL/Real/Rational.thy	Thu Sep 20 16:37:33 2007 +0200
@@ -684,10 +684,10 @@
 attach (term_of) {*
 fun term_of_rat (p, q) =
   let
-    val rT = @{typ rat}
+    val rT = Type ("Rational.rat", [])
   in
     if q = 1 orelse p = 0 then HOLogic.mk_number rT p
-    else @{term "op / \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"} $
+    else Const ("HOL.inverse_class.divide", rT --> rT --> rT) $
       HOLogic.mk_number rT p $ HOLogic.mk_number rT q
   end;
 *}