[Hol-checkins] CVS: hol98/src/experimental-kernel Term.sml,1.10,1.11 Type.sml,1.4,1.5

[Michael N. <mic...@us...>]

Update of /cvsroot/hol/hol98/src/experimental-kernel
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv1485/experimental-kernel

Modified Files:
	Term.sml Type.sml 
Log Message:
Fix for soundness bug; Globals.old changes its behaviour, and is no longer
a reference.  It is used in the kernel to do semantically significant things
so can't just be left to a user to change arbitrarily.


Index: Term.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/experimental-kernel/Term.sml,v
retrieving revision 1.10
retrieving revision 1.11
diff -b -C2 -d -r1.10 -r1.11
*** Term.sml	25 Oct 2004 07:10:40 -0000	1.10
--- Term.sml	25 Oct 2004 07:44:19 -0000	1.11
***************
*** 66,70 ****
  in
    const_table := newtable;
!   v := {Name = !Globals.old oldname, Thy = Thy, base_type = base_type,
          uptodate = false}
  end handle Map.NotFound =>
--- 66,70 ----
  in
    const_table := newtable;
!   v := {Name = Globals.old oldname, Thy = Thy, base_type = base_type,
          uptodate = false}
  end handle Map.NotFound =>

Index: Type.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/experimental-kernel/Type.sml,v
retrieving revision 1.4
retrieving revision 1.5
diff -b -C2 -d -r1.4 -r1.5
*** Type.sml	25 Oct 2004 07:10:40 -0000	1.4
--- Type.sml	25 Oct 2004 07:44:19 -0000	1.5
***************
*** 28,32 ****
  in
    operator_table := newtable;
!   v := {key = {Tyop = !Globals.old Tyop, Thy = Thy}, arity = arity,
          uptodate = false}
  end handle Map.NotFound => raise ERR "prim_delete_type" "No such type"
--- 28,32 ----
  in
    operator_table := newtable;
!   v := {key = {Tyop = Globals.old Tyop, Thy = Thy}, arity = arity,
          uptodate = false}
  end handle Map.NotFound => raise ERR "prim_delete_type" "No such type"