# HG changeset patch
# User wenzelm
# Date 865420002 -7200
# Node ID d8700b00894413a1849a4cff11e5cfd976737cc4
# Parent  fa31c7dca46863d4de8c8117feea73ac9d5ee85b
eliminated freeze_vars;

diff -r fa31c7dca468 -r d8700b008944 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Jun 04 10:58:56 1997 +0200
+++ b/src/Pure/axclass.ML	Wed Jun 04 12:26:42 1997 +0200
@@ -42,6 +42,10 @@
 
 fun aT S = TFree ("'a", S);
 
+fun dest_varT (TFree (x, S)) = ((x, ~1), S)
+  | dest_varT (TVar xi_S) = xi_S
+  | dest_varT T = raise_type "dest_varT" [T] [];
+
 
 (* get axioms and theorems *)
 
@@ -67,9 +71,9 @@
   let
     fun err () = raise_term "dest_classrel" [tm];
 
-    val (ty, c2) = Logic.dest_inclass (Logic.freeze_vars tm)
-	           handle TERM _ => err ();
-    val c1 = (case ty of TFree (_, [c]) => c | _ => err ());
+    val (ty, c2) = Logic.dest_inclass tm handle TERM _ => err ();
+    val c1 = (case dest_varT ty of (_, [c]) => c | _ => err ())
+      handle TYPE _ => err ();
   in
     (c1, c2)
   end;
@@ -89,15 +93,14 @@
   let
     fun err () = raise_term "dest_arity" [tm];
 
-    val (ty, c) = Logic.dest_inclass (Logic.freeze_vars tm) 
-	          handle TERM _ => err ();
-    val (t, tfrees) =
+    val (ty, c) = Logic.dest_inclass tm handle TERM _ => err ();
+    val (t, tvars) =
       (case ty of
-        Type (t, tys) => (t, map (fn TFree x => x | _ => err ()) tys)
+        Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ())
       | _ => err ());
     val ss =
-      if null (gen_duplicates eq_fst tfrees)
-      then map snd tfrees else err ();
+      if null (gen_duplicates eq_fst tvars)
+      then map snd tvars else err ();
   in
     (t, ss, c)
   end;