# HG changeset patch
# User wenzelm
# Date 877338361 -7200
# Node ID 1f1c1f524d196944402eec6ad53e4c0f1d00618e
# Parent  ea440c63d206eb29f4ae997183940cadaff75d48
adapted to qualified names;

diff -r ea440c63d206 -r 1f1c1f524d19 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Mon Oct 20 11:01:07 1997 +0200
+++ b/src/FOLP/IFOLP.thy	Mon Oct 20 11:06:01 1997 +0200
@@ -8,6 +8,8 @@
 
 IFOLP = Pure +
 
+global
+
 classes term < logic
 
 default term
@@ -59,6 +61,8 @@
  idpeel         :: "[p,'a=>p]=>p"
  nrm, NRM       :: "p"
 
+local
+
 rules
 
 (**** Propositional logic ****)
diff -r ea440c63d206 -r 1f1c1f524d19 src/FOLP/ROOT.ML
--- a/src/FOLP/ROOT.ML	Mon Oct 20 11:01:07 1997 +0200
+++ b/src/FOLP/ROOT.ML	Mon Oct 20 11:06:01 1997 +0200
@@ -12,6 +12,8 @@
 
 writeln banner;
 
+reset global_names;
+
 print_depth 1;
 
 use_thy "IFOLP";