# HG changeset patch
# User nipkow
# Date 864318557 -7200
# Node ID a106a557d704b9eecee1f1664fde42e64bd5eb62
# Parent  13d955a405f376582ff3e0f10ca551854f3e0d43
exhaust_tac can now deal with whole terms rather than just variables.

diff -r 13d955a405f3 -r a106a557d704 src/HOL/thy_data.ML
--- a/src/HOL/thy_data.ML	Thu May 22 17:20:55 1997 +0200
+++ b/src/HOL/thy_data.ML	Thu May 22 18:29:17 1997 +0200
@@ -68,6 +68,20 @@
             Some info => info
           | None => error ("Not a datatype: " ^ quote tn)
 
+fun infer_tname state sign i aterm =
+let val (_, _, Bi, _) = dest_state (state, i)
+    val params = Logic.strip_params Bi	        (*params of subgoal i*)
+    val params = rev(rename_wrt_term Bi params) (*as they are printed*)
+    val (types,sorts) = types_sorts state
+    fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
+      | types'(ixn) = types ixn;
+    val (ct,_) = read_def_cterm (sign,types',sorts) [] false
+                                (aterm,TVar(("",0),[]));
+in case #T(rep_cterm ct) of
+     Type(tn,_) => tn
+   | _ => error("Cannot induct on type of " ^ quote aterm)
+end;
+
 in
 
 (* generic induction tactic for datatypes *)
@@ -81,13 +95,12 @@
   in STATE induct end;
 
 (* generic exhaustion tactic for datatypes *)
-fun exhaust_tac var i =
+fun exhaust_tac aterm i =
   let fun exhaust state =
-        let val (_, _, Bi, _) = dest_state (state, i) 
-            val sign = #sign(rep_thm state)
-            val tn = find_tname var Bi
+        let val sign = #sign(rep_thm state)
+            val tn = infer_tname state sign i aterm
             val exh_tac = #exhaust_tac(get_dt_info sign tn)
-        in exh_tac var i end
+        in exh_tac aterm i end
   in STATE exhaust end;
 
 end;