deglobalization
authorhaftmann
Wed Aug 18 12:26:48 2010 +0200 (2010-08-18)
changeset 38522de7984a7172b
parent 38514 bd9c4e8281ec
child 38523 a2b7993a0529
deglobalization
NEWS
src/FOL/IFOL.thy
src/FOLP/IFOLP.thy
src/ZF/Datatype_ZF.thy
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/NEWS	Wed Aug 18 12:19:27 2010 +0200
     1.2 +++ b/NEWS	Wed Aug 18 12:26:48 2010 +0200
     1.3 @@ -131,6 +131,16 @@
     1.4  similar to inductive_cases.
     1.5  
     1.6  
     1.7 +*** FOL ***
     1.8 +
     1.9 +* All constant names are now qualified.  INCOMPATIBILITY.
    1.10 +
    1.11 +
    1.12 +*** ZF ***
    1.13 +
    1.14 +* All constant names are now qualified.  INCOMPATIBILITY.
    1.15 +
    1.16 +
    1.17  *** ML ***
    1.18  
    1.19  * ML antiquotations @{theory} and @{theory_ref} refer to named
     2.1 --- a/src/FOL/IFOL.thy	Wed Aug 18 12:19:27 2010 +0200
     2.2 +++ b/src/FOL/IFOL.thy	Wed Aug 18 12:26:48 2010 +0200
     2.3 @@ -28,8 +28,6 @@
     2.4  
     2.5  setup PureThy.old_appl_syntax_setup
     2.6  
     2.7 -global
     2.8 -
     2.9  classes "term"
    2.10  default_sort "term"
    2.11  
    2.12 @@ -87,8 +85,6 @@
    2.13    Ex        (binder "\<exists>" 10) and
    2.14    Ex1       (binder "\<exists>!" 10)
    2.15  
    2.16 -local
    2.17 -
    2.18  finalconsts
    2.19    False All Ex
    2.20    "op ="
     3.1 --- a/src/FOLP/IFOLP.thy	Wed Aug 18 12:19:27 2010 +0200
     3.2 +++ b/src/FOLP/IFOLP.thy	Wed Aug 18 12:26:48 2010 +0200
     3.3 @@ -12,8 +12,6 @@
     3.4  
     3.5  setup PureThy.old_appl_syntax_setup
     3.6  
     3.7 -global
     3.8 -
     3.9  classes "term"
    3.10  default_sort "term"
    3.11  
    3.12 @@ -63,8 +61,6 @@
    3.13   nrm            :: p
    3.14   NRM            :: p
    3.15  
    3.16 -local
    3.17 -
    3.18  syntax "_Proof" :: "[p,o]=>prop"    ("(_ /: _)" [51, 10] 5)
    3.19  
    3.20  ML {*
     4.1 --- a/src/ZF/Datatype_ZF.thy	Wed Aug 18 12:19:27 2010 +0200
     4.2 +++ b/src/ZF/Datatype_ZF.thy	Wed Aug 18 12:26:48 2010 +0200
     4.3 @@ -61,7 +61,7 @@
     4.4  struct
     4.5    val trace = Unsynchronized.ref false;
     4.6  
     4.7 -  fun mk_new ([],[]) = Const("True",FOLogic.oT)
     4.8 +  fun mk_new ([],[]) = Const(@{const_name True},FOLogic.oT)
     4.9      | mk_new (largs,rargs) =
    4.10          Balanced_Tree.make FOLogic.mk_conj
    4.11                   (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
    4.12 @@ -85,7 +85,7 @@
    4.13             if #big_rec_name lcon_info = #big_rec_name rcon_info
    4.14                 andalso not (null (#free_iffs lcon_info)) then
    4.15                 if lname = rname then mk_new (largs, rargs)
    4.16 -               else Const("False",FOLogic.oT)
    4.17 +               else Const(@{const_name False},FOLogic.oT)
    4.18             else raise Match
    4.19         val _ =
    4.20           if !trace then writeln ("NEW = " ^ Syntax.string_of_term_global sg new)
     5.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Aug 18 12:19:27 2010 +0200
     5.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Aug 18 12:26:48 2010 +0200
     5.3 @@ -118,7 +118,7 @@
     5.4  fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
     5.5    let
     5.6      (*analyze the LHS of a case equation to get a constructor*)
     5.7 -    fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
     5.8 +    fun const_of (Const(@{const_name "op ="}, _) $ (_ $ c) $ _) = c
     5.9        | const_of eqn = error ("Ill-formed case equation: " ^
    5.10                                Syntax.string_of_term_global thy eqn);
    5.11  
     6.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Aug 18 12:19:27 2010 +0200
     6.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Aug 18 12:26:48 2010 +0200
     6.3 @@ -102,7 +102,7 @@
     6.4  
     6.5    val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
     6.6  
     6.7 -  fun dest_tprop (Const("Trueprop",_) $ P) = P
     6.8 +  fun dest_tprop (Const(@{const_name Trueprop},_) $ P) = P
     6.9      | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
    6.10                              Syntax.string_of_term ctxt Q);
    6.11  
     7.1 --- a/src/ZF/Tools/typechk.ML	Wed Aug 18 12:19:27 2010 +0200
     7.2 +++ b/src/ZF/Tools/typechk.ML	Wed Aug 18 12:26:48 2010 +0200
     7.3 @@ -75,7 +75,7 @@
     7.4           if length rls <= maxr then resolve_tac rls i else no_tac
     7.5        end);
     7.6  
     7.7 -fun is_rigid_elem (Const("Trueprop",_) $ (Const(@{const_name mem},_) $ a $ _)) =
     7.8 +fun is_rigid_elem (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) =
     7.9        not (is_Var (head_of a))
    7.10    | is_rigid_elem _ = false;
    7.11