src/HOLCF/IOA/ex/TrivEx.thy

--- a/src/HOLCF/IOA/ex/TrivEx.thy	Fri Mar 20 11:26:59 2009 +0100
+++ b/src/HOLCF/IOA/ex/TrivEx.thy	Fri Mar 20 15:24:18 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/IOA/TrivEx.thy
-    ID:         $Id$
     Author:     Olaf Müller
 *)
 
@@ -66,7 +65,7 @@
 apply (rule AbsRuleT1)
 apply (rule h_abs_is_abstraction)
 apply (rule MC_result)
-apply (tactic "abstraction_tac 1")
+apply abstraction
 apply (simp add: h_abs_def)
 done