# HG changeset patch
# User wenzelm
# Date 1248372320 -7200
# Node ID 53716a67c3b1251a9fde6091bcfa5d7555ff08fa
# Parent  2f65c45c2e7e5f34bed10627658091a4d1a16aac
global_claset_of;

diff -r 2f65c45c2e7e -r 53716a67c3b1 src/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Jul 23 18:44:10 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Jul 23 20:05:20 2009 +0200
@@ -399,7 +399,7 @@
       ==> input_enabled (A||B)"
 apply (unfold input_enabled_def)
 apply (simp add: Let_def inputs_of_par trans_of_par)
-apply (tactic "safe_tac (claset_of @{theory Fun})")
+apply (tactic "safe_tac (global_claset_of @{theory Fun})")
 apply (simp add: inp_is_act)
 prefer 2
 apply (simp add: inp_is_act)