# HG changeset patch
# User paulson
# Date 818414609 -3600
# Node ID bf523422a3dffe2577e302a30a8163cc2e8bd629
# Parent  fbe857ddc80de7c11a8ebfad9f6de6a484796b00
Commented and renamed vars in readtm

diff -r fbe857ddc80d -r bf523422a3df src/Pure/section_utils.ML
--- a/src/Pure/section_utils.ML	Thu Dec 07 18:36:33 1995 +0100
+++ b/src/Pure/section_utils.ML	Fri Dec 08 10:23:29 1995 +0100
@@ -24,9 +24,10 @@
 (*Read an assumption in the given theory*)
 fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
 
-fun readtm sign T a = 
-    read_cterm sign (a,T) |> term_of
-    handle ERROR => error ("The error above occurred for " ^ a);
+(*Read a term from string "b", with expected type T*)
+fun readtm sign T b = 
+    read_cterm sign (b,T) |> term_of
+    handle ERROR => error ("The error above occurred for " ^ b);
 
 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))