# HG changeset patch
# User haftmann
# Date 1145889367 -7200
# Node ID d828bfab05af7962cafc1faa0700096b4454f9b4
# Parent  46a7e133f8027a28dc2ec9ef41c5b343047dc5a0
cleaned up some diagnostic mathom

diff -r 46a7e133f802 -r d828bfab05af src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Mon Apr 24 16:35:30 2006 +0200
+++ b/src/Pure/tctical.ML	Mon Apr 24 16:36:07 2006 +0200
@@ -482,36 +482,34 @@
   in SOME (map (forall_elim_vars 0 o assume o cterm) hyps) end
   handle TERM ("nth_prem", [A]) => NONE;
 
-
-fun find_vars thy (Const(c,tp)) vars =
-    let val tvars = Term.typ_tvars tp
-    in
-	case tvars of [] => vars
-		    | _ => insert (op =) (c ^ " has type: " ^ (Sign.string_of_typ thy tp)) vars
-    end
-  | find_vars thy (t as Var(_,_)) vars =
-    insert (op =) ("Var " ^ (Term.str_of_term t)) vars
-  | find_vars _ (Free(_,_)) vars = vars
-  | find_vars _ (Bound _) vars = vars
-  | find_vars thy (Abs(_,tp,b)) vars = find_vars thy b vars
-  | find_vars thy (t1 $ t2) vars = 
-    find_vars thy t2 (find_vars thy t1 vars);
-
-  
-fun warning_multi [] = ()
-  | warning_multi (str1::strs) =
-    (warning str1; warning_multi strs);
+local
 
 fun print_vars_terms thy (n,thm) =
-    let val prem = Logic.nth_prem (n, Thm.prop_of thm)
-	val tms = find_vars thy prem []
-    in
-	(warning "Found schematic vars in assumptions: "; warning_multi tms)
-    end;
+  let
+    fun find_vars thy (Const (c, ty)) =
+        (case Term.typ_tvars ty
+         of [] => I
+          | _ => insert (op =) (c ^ " has type: " ^ (Sign.string_of_typ thy ty)))
+      | find_vars thy (t as Var _) =
+          insert (op =) ("Var " ^ (Term.str_of_term t))
+      | find_vars _ (Free _) = I
+      | find_vars _ (Bound _) = I
+      | find_vars thy (Abs (_, _, t)) = find_vars thy t
+      | find_vars thy (t1 $ t2) = 
+          find_vars thy t1 #> find_vars thy t1;
+    val prem = Logic.nth_prem (n, Thm.prop_of thm)
+    val tms = find_vars thy prem []
+  in
+    (warning "Found schematic vars in assumptions:"; warning (cat_lines tms))
+  end;
+
+in
 
 fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
     handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty)
 
+end; (*local*)
+
 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
 fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
 
@@ -520,7 +518,7 @@
 
 (* Inverse (more or less) of PRIMITIVE *)
 fun SINGLE tacf = Option.map fst o Seq.pull o tacf
-		  
+
 end;
 
 open Tactical;
diff -r 46a7e133f802 -r d828bfab05af src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Apr 24 16:35:30 2006 +0200
+++ b/src/Pure/term.ML	Mon Apr 24 16:36:07 2006 +0200
@@ -209,6 +209,8 @@
   val adhoc_freeze_vars: term -> term * string list
   val string_of_vname: indexname -> string
   val string_of_vname': indexname -> string
+  val str_of_sort: sort -> string
+  val str_of_typ: typ -> string
   val str_of_term: term -> string
 end;
 
@@ -1312,8 +1314,6 @@
   in (subst_atomic insts tm, xs) end;
 
 
-(* string_of_vname *)
-
 val show_question_marks = ref true;
 
 fun string_of_vname (x, i) =
@@ -1335,15 +1335,36 @@
 fun string_of_vname' (x, ~1) = x
   | string_of_vname' xi = string_of_vname xi;
 
-
-(* str_of_term *)
+fun str_of_sort [] = "{}"
+  | str_of_sort [c] = c
+  | str_of_sort cs = (enclose "{" "}" o commas) cs
 
-fun str_of_term (Const (c, _)) = c
-  | str_of_term (Free (x, _)) = x
-  | str_of_term (Var (xi, _)) = string_of_vname xi
-  | str_of_term (Bound i) = string_of_int i
-  | str_of_term (Abs (x, _, t)) = "%" ^ x ^ ". " ^ str_of_term t
-  | str_of_term (t $ u) = "(" ^ str_of_term t ^ " " ^ str_of_term u ^ ")";
+fun str_of_typ (Type ("fun", [ty1, ty2])) =
+      "(" ^ str_of_typ ty1 ^ " => " ^ str_of_typ ty2 ^ ")"
+  | str_of_typ (Type ("dummy", [])) =
+      "_"
+  | str_of_typ (Type (tyco, _)) =
+      tyco
+  | str_of_typ (Type (tyco, tys)) =
+      (enclose "(" ")" o space_implode " ") (tyco :: map str_of_typ tys)
+  | str_of_typ (TFree (v, sort)) =
+      v ^ "::" ^ str_of_sort sort
+  | str_of_typ (TVar (vi, sort)) =
+      string_of_vname vi ^ "::" ^ str_of_sort sort;
+
+val str_of_term =
+  let
+    fun typed (s, ty) = s ^ "::" ^ str_of_typ ty;
+    fun bound vs i = case AList.lookup (op =) vs i
+     of SOME v => enclose "[" "]" (string_of_int i ^ " ~> " ^ v)
+      | NONE => (enclose "[" "]" o string_of_int) i
+    fun str vs (Const (c, _)) = c
+      | str vs (Free (v, ty)) = typed (v, ty)
+      | str vs (Var (vi, ty)) = typed (string_of_vname vi, ty)
+      | str vs (Bound i) = bound vs i
+      | str vs (Abs (x, ty, t)) = "(%" ^ typed (x, ty) ^ ". " ^ str ((length vs, x)::vs) t ^ ")"
+      | str vs (t1 $ t2) = "(" ^ str vs t1 ^ " " ^ str vs t2 ^ ")";
+  in str [] end;
 
 end;