# HG changeset patch
# User wenzelm
# Date 1149537264 -7200
# Node ID f0a318495ca4fa2a88eabf1cf4fbd10fbe9ae2b0
# Parent  77929c3d2b747df3892066173dc58d2965aa31eb
assm_tac: try rule termI;

diff -r 77929c3d2b74 -r f0a318495ca4 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Jun 05 21:54:23 2006 +0200
+++ b/src/Pure/Isar/method.ML	Mon Jun 05 21:54:24 2006 +0200
@@ -219,14 +219,15 @@
 fun asm_tac ths =
   foldr (op APPEND') (K no_tac) (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths);
 
-val refl_tac = SUBGOAL (fn (prop, i) =>
-  if can Logic.dest_equals (Logic.strip_assums_concl prop)
-  then Tactic.rtac Drule.reflexive_thm i else no_tac);
+fun cond_rtac cond rule = SUBGOAL (fn (prop, i) =>
+  if cond (Logic.strip_assums_concl prop)
+  then Tactic.rtac rule i else no_tac);
 
 fun assm_tac ctxt =
   assume_tac APPEND'
   asm_tac (ProofContext.prems_of ctxt) APPEND'
-  refl_tac;
+  cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
+  cond_rtac (can Logic.dest_term) Drule.termI;
 
 fun assumption_tac ctxt [] = assm_tac ctxt
   | assumption_tac _ [fact] = asm_tac [fact]