src/HOL/Bali/TypeRel.thy
changeset 60754 02924903a6fd
parent 58887 38db8ddc0f57
child 61989 ba8c284d4725
--- a/src/HOL/Bali/TypeRel.thy	Sat Jul 18 20:53:05 2015 +0200
+++ b/src/HOL/Bali/TypeRel.thy	Sat Jul 18 20:54:56 2015 +0200
@@ -535,7 +535,7 @@
 apply      safe
 apply            (rule widen.int_obj)
 prefer          6 apply (drule implmt_is_class) apply simp
-apply (tactic "ALLGOALS (etac thin_rl)")
+apply (erule_tac [!] thin_rl)
 prefer         6 apply simp
 apply          (rule_tac [9] widen.arr_obj)
 apply         (rotate_tac [9] -1)