removed obsolete inst;
authorwenzelm
Mon Jun 16 17:54:47 2008 +0200 (2008-06-16)
changeset 27233224c830e7abe
parent 27232 7cd256da0a36
child 27234 e60cdbc5e8e1
removed obsolete inst;
src/Pure/old_goals.ML
     1.1 --- a/src/Pure/old_goals.ML	Mon Jun 16 17:54:46 2008 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Mon Jun 16 17:54:47 2008 +0200
     1.3 @@ -81,7 +81,6 @@
     1.4    val fds: thm list -> unit
     1.5    val fd: thm -> unit
     1.6    val fa: unit -> unit
     1.7 -  val inst: string -> string -> thm -> thm
     1.8  end;
     1.9  
    1.10  structure OldGoals: OLD_GOALS =
    1.11 @@ -517,9 +516,6 @@
    1.12  
    1.13  fun no_qed () = ();
    1.14  
    1.15 -(*shorthand for instantiating just one variable in the current theory*)
    1.16 -fun inst x t = Drule.read_instantiate_sg (ML_Context.the_global_context()) [(x,t)];
    1.17 -
    1.18  end;
    1.19  
    1.20  structure Goals: GOALS = OldGoals;