tuned;

--- a/src/Pure/Isar/element.ML	Tue Jul 30 15:09:25 2013 +0200
+++ b/src/Pure/Isar/element.ML	Tue Jul 30 15:20:38 2013 +0200
@@ -395,7 +395,7 @@
    {binding = [],
     typ = [instT_type env],
     term = [instT_term env],
-    fact = [map (fn th => instT_thm thy env th)]};
+    fact = [map (instT_thm thy env)]};
 
 
 (* instantiate types and terms *)
@@ -438,7 +438,7 @@
    {binding = [],
     typ = [instT_type envT],
     term = [inst_term (envT, env)],
-    fact = [map (fn th => inst_thm thy (envT, env) th)]};
+    fact = [map (inst_thm thy (envT, env))]};
 
 
 (* satisfy hypotheses *)

--- a/src/Pure/thm.ML	Tue Jul 30 15:09:25 2013 +0200
+++ b/src/Pure/thm.ML	Tue Jul 30 15:20:38 2013 +0200
@@ -978,7 +978,7 @@
             tpairs = union_tpairs tpairs1 tpairs2,
             prop = B})
         else err "not equal"
-     | _ =>  err"major premise")
+     | _ =>  err "major premise")
   end;