# HG changeset patch
# User wenzelm
# Date 981056711 -3600
# Node ID 41de937d338b5c818c92aa40b1ab509776e6fd20
# Parent  646c929b629315e99ee54827340789194573d2e2
comment

diff -r 646c929b6293 -r 41de937d338b src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Feb 01 20:44:19 2001 +0100
+++ b/src/Pure/Isar/obtain.ML	Thu Feb 01 20:45:11 2001 +0100
@@ -11,7 +11,7 @@
 
   {
     fix thesis
-    assume that: "!!x. P x ==> thesis"
+    assume that [intro]: "!!x. P x ==> thesis"
     <chain_facts> have thesis <proof (insert that)>
   }
   fix x assm (obtained) "P x"
diff -r 646c929b6293 -r 41de937d338b src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Feb 01 20:44:19 2001 +0100
+++ b/src/Pure/library.ML	Thu Feb 01 20:45:11 2001 +0100
@@ -271,7 +271,7 @@
   val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
   val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
   val transitive_closure: (string * string list) list -> (string * string list) list
-  val init_gensym: unit -> unit
+  val init_gensym: unit -> unit    (* FIXME !!??! *)
   val gensym: string -> string
   val bump_int_list: string list -> string list
   val bump_list: string list * string -> string list
@@ -1344,7 +1344,7 @@
 
 in
 
-fun init_gensym() = (seedr := 0);
+fun init_gensym() = (seedr := 0);    (* FIXME !!??! *)
 
 fun gensym pre = pre ^ (#1(newid (!seedr), inc seedr));
 end;