removed load;
authorwenzelm
Wed Feb 03 16:49:04 1999 +0100 (1999-02-03 ago)
changeset 619562dc7e9050eb
parent 6194 358f62acf573
child 6196 f9fdb4e29790
removed load;
proper use (ThyInfo.load_file);
added use_thy, update_thy;
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Feb 03 16:48:17 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Feb 03 16:49:04 1999 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    val cd: string -> Toplevel.transition -> Toplevel.transition
     1.5    val pwd: Toplevel.transition -> Toplevel.transition
     1.6    val use_thy: string -> Toplevel.transition -> Toplevel.transition
     1.7 -  val load: string -> Toplevel.transition -> Toplevel.transition
     1.8 +  val update_thy: string -> Toplevel.transition -> Toplevel.transition
     1.9    val print_theory: Toplevel.transition -> Toplevel.transition
    1.10    val print_syntax: Toplevel.transition -> Toplevel.transition
    1.11    val print_theorems: Toplevel.transition -> Toplevel.transition
    1.12 @@ -51,7 +51,7 @@
    1.13  
    1.14  (* use ML text *)
    1.15  
    1.16 -fun use name = Toplevel.imperative (fn () => Use.use name);
    1.17 +fun use name = Toplevel.imperative (fn () => ThyInfo.load_file (Path.unpack name));
    1.18  
    1.19  (*passes changes of theory context*)
    1.20  val use_mltext_theory = Toplevel.theory o IsarThy.use_mltext_theory;
    1.21 @@ -74,10 +74,8 @@
    1.22  
    1.23  (* load theory files *)
    1.24  
    1.25 -fun use_thy name = Toplevel.imperative (fn () => ThyRead.use_thy name);
    1.26 -
    1.27 -fun load name =
    1.28 -  Toplevel.imperative (fn () => Toplevel.excursion (OuterSyntax.read_file (name ^ ".thy")));
    1.29 +fun use_thy name = Toplevel.imperative (fn () => ThyInfo.use_thy name);
    1.30 +fun update_thy name = Toplevel.imperative (fn () => ThyInfo.update_thy name);
    1.31  
    1.32  
    1.33  (* print theory contents *)