src/ZF/Datatype_ZF.thy
changeset 38522 de7984a7172b
parent 35409 5c5bb83f2bae
child 38715 6513ea67d95d
     1.1 --- a/src/ZF/Datatype_ZF.thy	Wed Aug 18 12:19:27 2010 +0200
     1.2 +++ b/src/ZF/Datatype_ZF.thy	Wed Aug 18 12:26:48 2010 +0200
     1.3 @@ -61,7 +61,7 @@
     1.4  struct
     1.5    val trace = Unsynchronized.ref false;
     1.6  
     1.7 -  fun mk_new ([],[]) = Const("True",FOLogic.oT)
     1.8 +  fun mk_new ([],[]) = Const(@{const_name True},FOLogic.oT)
     1.9      | mk_new (largs,rargs) =
    1.10          Balanced_Tree.make FOLogic.mk_conj
    1.11                   (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
    1.12 @@ -85,7 +85,7 @@
    1.13             if #big_rec_name lcon_info = #big_rec_name rcon_info
    1.14                 andalso not (null (#free_iffs lcon_info)) then
    1.15                 if lname = rname then mk_new (largs, rargs)
    1.16 -               else Const("False",FOLogic.oT)
    1.17 +               else Const(@{const_name False},FOLogic.oT)
    1.18             else raise Match
    1.19         val _ =
    1.20           if !trace then writeln ("NEW = " ^ Syntax.string_of_term_global sg new)