# HG changeset patch
# User paulson
# Date 910960190 -3600
# Node ID 701498a38a7623281008552b2fa9a9f78eb5e70a
# Parent  5fb5a626f3b942980e8e0f41bad39a96f7a41f8b
qualified the name "restrict" since Fun.restrict exists too

diff -r 5fb5a626f3b9 -r 701498a38a76 src/HOLCF/IOA/NTP/Correctness.ML
--- a/src/HOLCF/IOA/NTP/Correctness.ML	Fri Nov 13 13:29:04 1998 +0100
+++ b/src/HOLCF/IOA/NTP/Correctness.ML	Fri Nov 13 13:29:50 1998 +0100
@@ -28,7 +28,7 @@
  * to that of the specification.
  ****************************)
 Goal
- "a:externals(asig_of(restrict impl_ioa (externals spec_sig))) = \
+ "a:externals(asig_of(Automata.restrict impl_ioa (externals spec_sig))) = \
 \ (case a of                  \
 \     S_msg(m) => True        \
 \   | R_msg(m) => True        \
@@ -67,7 +67,8 @@
 
 (* Proof of correctness *)
 Goalw [Spec.ioa_def, is_weak_ref_map_def]
-  "is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
+  "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig))  \
+\                  spec_ioa";
 by (simp_tac (simpset() delsplits [split_if] addsimps 
     [Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
 by (rtac conjI 1);