src/Pure/Thy/context.ML
changeset 5059 dcdb21e53537
parent 5049 bde086cfa597
child 5249 9d7e6f7110ef
     1.1 --- a/src/Pure/Thy/context.ML	Sat Jun 20 20:18:22 1998 +0200
     1.2 +++ b/src/Pure/Thy/context.ML	Sat Jun 20 20:18:51 1998 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  sig
     1.5    val context: theory -> unit
     1.6    val the_context: unit -> theory
     1.7 -  val Thm: xstring -> thm
     1.8 -  val Thms: xstring -> thm list
     1.9 +  val thm: xstring -> thm
    1.10 +  val thms: xstring -> thm list
    1.11    val Goal: string -> thm list
    1.12    val Goalw: thm list -> string -> thm list
    1.13  end;
    1.14 @@ -73,8 +73,8 @@
    1.15  
    1.16  (* retrieve thms *)
    1.17  
    1.18 -fun Thm name = PureThy.get_thm (the_context ()) name;
    1.19 -fun Thms name = PureThy.get_thms (the_context ()) name;
    1.20 +fun thm name = PureThy.get_thm (the_context ()) name;
    1.21 +fun thms name = PureThy.get_thms (the_context ()) name;
    1.22  
    1.23  
    1.24  (* shortcut goal commands *)