# HG changeset patch
# User haftmann
# Date 1282126767 -7200
# Node ID bd9c4e8281ecbd58e2f501136600f5c1aebd3092
# Parent  33ab01218ae192b31c6ef44ddad58660f1a3fc61
deglobalization

diff -r 33ab01218ae1 -r bd9c4e8281ec src/ZF/Inductive_ZF.thy
--- a/src/ZF/Inductive_ZF.thy	Wed Aug 18 12:08:21 2010 +0200
+++ b/src/ZF/Inductive_ZF.thy	Wed Aug 18 12:19:27 2010 +0200
@@ -31,8 +31,8 @@
 lemma refl_thin: "!!P. a = a ==> P ==> P" .
 
 use "ind_syntax.ML"
+use "Tools/ind_cases.ML"
 use "Tools/cartprod.ML"
-use "Tools/ind_cases.ML"
 use "Tools/inductive_package.ML"
 use "Tools/induct_tacs.ML"
 use "Tools/primrec_package.ML"
diff -r 33ab01218ae1 -r bd9c4e8281ec src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Wed Aug 18 12:08:21 2010 +0200
+++ b/src/ZF/Sum.thy	Wed Aug 18 12:19:27 2010 +0200
@@ -9,8 +9,6 @@
 
 text{*And the "Part" primitive for simultaneous recursive type definitions*}
 
-global
-
 definition sum :: "[i,i]=>i" (infixr "+" 65) where
      "A+B == {0}*A Un {1}*B"
 
@@ -27,8 +25,6 @@
 definition Part :: "[i,i=>i] => i" where
      "Part(A,h) == {x: A. EX z. x = h(z)}"
 
-local
-
 subsection{*Rules for the @{term Part} Primitive*}
 
 lemma Part_iff: 
diff -r 33ab01218ae1 -r bd9c4e8281ec src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Wed Aug 18 12:08:21 2010 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Wed Aug 18 12:19:27 2010 +0200
@@ -115,8 +115,8 @@
             case AList.lookup (op =) eqns cname of
                 NONE => (warning ("no equation for constructor " ^ cname ^
                                   "\nin definition of function " ^ fname);
-                         (Const ("0", Ind_Syntax.iT),
-                          #2 recursor_pair, Const ("0", Ind_Syntax.iT)))
+                         (Const (@{const_name 0}, Ind_Syntax.iT),
+                          #2 recursor_pair, Const (@{const_name 0}, Ind_Syntax.iT)))
               | SOME (rhs, cargs', eq) =>
                     (rhs, inst_recursor (recursor_pair, cargs'), eq)
           val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
diff -r 33ab01218ae1 -r bd9c4e8281ec src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Wed Aug 18 12:08:21 2010 +0200
+++ b/src/ZF/ZF.thy	Wed Aug 18 12:19:27 2010 +0200
@@ -12,8 +12,6 @@
 
 ML {* Unsynchronized.reset eta_contract *}
 
-global
-
 typedecl i
 arities  i :: "term"
 
@@ -209,8 +207,6 @@
   subset_def:    "A <= B == \<forall>x\<in>A. x\<in>B"
 
 
-local
-
 axioms
 
   (* ZF axioms -- see Suppes p.238
diff -r 33ab01218ae1 -r bd9c4e8281ec src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Wed Aug 18 12:08:21 2010 +0200
+++ b/src/ZF/ind_syntax.ML	Wed Aug 18 12:19:27 2010 +0200
@@ -18,7 +18,7 @@
 
 (** Abstract syntax definitions for ZF **)
 
-val iT = Type("i",[]);
+val iT = Type(@{type_name i}, []);
 
 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
 fun mk_all_imp (A,P) =