src/Pure/Isar/toplevel.ML
changeset 37937 9e482a3e651e
parent 37906 4195727a1f6c
child 37949 48a874444164
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Jul 22 18:08:39 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Jul 22 20:36:41 2010 +0200
     1.3 @@ -632,7 +632,7 @@
     1.4  fun run_command thy_name tr st =
     1.5    (case
     1.6        (case init_of tr of
     1.7 -        SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
     1.8 +        SOME name => Exn.capture (fn () => Thy_Load.consistent_name thy_name name) ()
     1.9        | NONE => Exn.Result ()) of
    1.10      Exn.Result () =>
    1.11        let val int = is_some (init_of tr) in