# HG changeset patch
# User paulson
# Date 1117795288 -7200
# Node ID ee95ab217fee0a30b3525de8060cd562d8873017
# Parent  cfd070a2cc4d2cd72431f89e63327bc15da91a55
no longer emits literals for type class HOL.type; also minor tidying

diff -r cfd070a2cc4d -r ee95ab217fee src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Fri Jun 03 01:08:07 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML	Fri Jun 03 12:41:28 2005 +0200
@@ -61,7 +61,7 @@
 val const_prefix = "const_";
 val tconst_prefix = "tconst_"; 
 
-val class_prefix = "clas_"; 
+val class_prefix = "class_"; 
 
 
 
@@ -358,36 +358,35 @@
 
 fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]));
     
- 
+(*Make literals for sorted type variables*) 
 fun sorts_on_typs (_, []) = []
-  | sorts_on_typs ((FOLTVar(indx)), [s]) = [LTVar((make_type_class s) ^ "(" ^ (make_schematic_type_var(string_of_indexname indx)) ^ ")")]
-  | sorts_on_typs ((FOLTVar(indx)), (s::ss))=  LTVar((make_type_class s) ^ "(" ^ (make_schematic_type_var(string_of_indexname indx)) ^ ")") :: (sorts_on_typs ((FOLTVar(indx)), ss))
-  | sorts_on_typs ((FOLTFree(x)), [s]) = [LTFree((make_type_class s) ^ "(" ^ (make_fixed_type_var(x)) ^ ")")]
-  | sorts_on_typs ((FOLTFree(x)), (s::ss)) = LTFree((make_type_class s) ^ "(" ^ (make_fixed_type_var(x)) ^ ")") :: (sorts_on_typs ((FOLTFree(x)), ss));
+  | sorts_on_typs (v, "HOL.type" :: s) =
+      sorts_on_typs (v,s)   (*Ignore sort "type"*)
+  | sorts_on_typs ((FOLTVar(indx)), (s::ss)) =
+      LTVar((make_type_class s) ^ 
+        "(" ^ (make_schematic_type_var(string_of_indexname indx)) ^ ")") :: 
+      (sorts_on_typs ((FOLTVar(indx)), ss))
+  | sorts_on_typs ((FOLTFree(x)), (s::ss)) =
+      LTFree((make_type_class s) ^ "(" ^ (make_fixed_type_var(x)) ^ ")") :: 
+      (sorts_on_typs ((FOLTFree(x)), ss));
 
-
+(*Given a list of sorted type variables, return two separate lists.
+  The first is for TVars, the second for TFrees.*)
 fun add_typs_aux [] = ([],[])
   | add_typs_aux ((FOLTVar(indx),s)::tss) = 
-    let val vs = sorts_on_typs (FOLTVar(indx),s)
-        val (vss,fss) = add_typs_aux tss
-    in
-        (ResLib.no_rep_app vs vss,fss)
-    end
+      let val vs = sorts_on_typs (FOLTVar(indx), s)
+	  val (vss,fss) = add_typs_aux tss
+      in
+	  (ResLib.no_rep_app vs vss, fss)
+      end
   | add_typs_aux ((FOLTFree(x),s)::tss) =
-    let val fs = sorts_on_typs (FOLTFree(x),s)
-        val (vss,fss) = add_typs_aux tss
-    in
-        (vss,ResLib.no_rep_app fs fss)
-    end;
-
+      let val fs = sorts_on_typs (FOLTFree(x), s)
+	  val (vss,fss) = add_typs_aux tss
+      in
+	  (vss, ResLib.no_rep_app fs fss)
+      end;
 
-fun add_typs (Clause cls) = 
-    let val ts = #types_sorts cls
-    in
-	add_typs_aux ts
-    end;    
-
-
+fun add_typs (Clause cls) = add_typs_aux (#types_sorts cls)
 
 
 (** make axiom clauses, hypothesis clauses and conjecture clauses. **)