src/HOL/TLA/ROOT.ML
changeset 3945 ae9c61d69888
parent 3807 82a99b090d9d
child 4477 b3e5857d8d99
     1.1 --- a/src/HOL/TLA/ROOT.ML	Mon Oct 20 11:14:16 1997 +0200
     1.2 +++ b/src/HOL/TLA/ROOT.ML	Mon Oct 20 11:14:55 1997 +0200
     1.3 @@ -12,6 +12,8 @@
     1.4  *)
     1.5  Syntax.ambiguity_level := 10000;
     1.6  
     1.7 +reset global_names;
     1.8 +
     1.9  use_thy "TLA";
    1.10  
    1.11  val TLA_build_completed = ();