# HG changeset patch
# User wenzelm
# Date 958643037 -7200
# Node ID 9df44a4f1bf7f064fa9c3a9099a7879fad0db42f
# Parent  0467dd0d66ff2aff496f98f0f01a9a0f5169bc9b
fewer consts declared as global;

diff -r 0467dd0d66ff -r 9df44a4f1bf7 TFL/rules.sml
--- a/TFL/rules.sml	Thu May 18 11:40:57 2000 +0200
+++ b/TFL/rules.sml	Thu May 18 11:43:57 2000 +0200
@@ -427,7 +427,7 @@
   let val {prop, ...} = rep_thm thm
   in case prop 
      of (Const("==>",_)$(Const("Trueprop",_)$ _) $
-         (Const("==",_) $ (Const ("cut",_) $ f $ R $ a $ x) $ _)) => false
+         (Const("==",_) $ (Const ("WF.cut",_) $ f $ R $ a $ x) $ _)) => false
       | _ => true
   end;
 
@@ -631,7 +631,7 @@
   end;
 
 fun restricted t = is_some (S.find_term
-			    (fn (Const("cut",_)) =>true | _ => false) 
+			    (fn (Const("WF.cut",_)) =>true | _ => false) 
 			    t)
 
 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
diff -r 0467dd0d66ff -r 9df44a4f1bf7 TFL/usyntax.sml
--- a/TFL/usyntax.sml	Thu May 18 11:40:57 2000 +0200
+++ b/TFL/usyntax.sml	Thu May 18 11:43:57 2000 +0200
@@ -321,7 +321,7 @@
                                   mesg="unexpected term structure"}
    else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
 
-fun is_WFR (Const("wf",_)$_) = true
+fun is_WFR (Const("WF.wf",_)$_) = true
   | is_WFR _                 = false;
 
 fun ARB ty = mk_select{Bvar=Free("v",ty),
diff -r 0467dd0d66ff -r 9df44a4f1bf7 src/HOL/Gfp.thy
--- a/src/HOL/Gfp.thy	Thu May 18 11:40:57 2000 +0200
+++ b/src/HOL/Gfp.thy	Thu May 18 11:43:57 2000 +0200
@@ -8,12 +8,8 @@
 
 Gfp = Lfp +
 
-global
-
 constdefs
   gfp :: ['a set=>'a set] => 'a set
   "gfp(f) == Union({u. u <= f(u)})"    (*greatest fixed point*)
 
-local
-
 end
diff -r 0467dd0d66ff -r 9df44a4f1bf7 src/HOL/Lfp.thy
--- a/src/HOL/Lfp.thy	Thu May 18 11:40:57 2000 +0200
+++ b/src/HOL/Lfp.thy	Thu May 18 11:43:57 2000 +0200
@@ -8,12 +8,8 @@
 
 Lfp = mono + Prod +
 
-global
-
 constdefs
   lfp :: ['a set=>'a set] => 'a set
   "lfp(f) == Inter({u. f(u) <= u})"    (*least fixed point*)
 
-local
-
 end
diff -r 0467dd0d66ff -r 9df44a4f1bf7 src/HOL/Ord.thy
--- a/src/HOL/Ord.thy	Thu May 18 11:40:57 2000 +0200
+++ b/src/HOL/Ord.thy	Thu May 18 11:43:57 2000 +0200
@@ -12,26 +12,26 @@
 axclass
   ord < term
 
-global
-
 syntax
   "op <"        :: ['a::ord, 'a] => bool             ("op <")
   "op <="       :: ['a::ord, 'a] => bool             ("op <=")
 
+global
+
 consts
   "op <"        :: ['a::ord, 'a] => bool             ("(_/ < _)"  [50, 51] 50)
   "op <="       :: ['a::ord, 'a] => bool             ("(_/ <= _)" [50, 51] 50)
-  mono          :: ['a::ord => 'b::ord] => bool       (*monotonicity*)
-  min, max      :: ['a::ord, 'a] => 'a
 
-  Least         :: ('a::ord=>bool) => 'a             (binder "LEAST " 10)
+local
 
 syntax (symbols)
   "op <="       :: ['a::ord, 'a] => bool             ("op \\<le>")
   "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
 
-
-local
+consts
+  mono          :: ['a::ord => 'b::ord] => bool      (*monotonicity*)
+  min, max      :: ['a::ord, 'a] => 'a
+  Least         :: ('a::ord=>bool) => 'a             (binder "LEAST " 10)
 
 defs
   mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
diff -r 0467dd0d66ff -r 9df44a4f1bf7 src/HOL/WF.thy
--- a/src/HOL/WF.thy	Thu May 18 11:40:57 2000 +0200
+++ b/src/HOL/WF.thy	Thu May 18 11:43:57 2000 +0200
@@ -8,8 +8,6 @@
 
 WF = Trancl +
 
-global
-
 constdefs
   wf         :: "('a * 'a)set => bool"
   "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
@@ -30,6 +28,4 @@
   "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
                             r x)  x)"
 
-local
-
 end