redundant: read = check o parse;

--- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Mon Jun 15 15:33:38 2015 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Mon Jun 15 15:34:29 2015 +0200
@@ -85,15 +85,13 @@
 
     val typs =
       map snd type_insts
-      |> Syntax.read_typs ctxt1
-      |> Syntax.check_typs ctxt1;
+      |> Syntax.read_typs ctxt1;
 
     val typ_insts' = map2 (fn (xi, _) => fn T => (xi,T)) type_insts typs;
 
     val terms =
       map snd term_insts
-      |> Syntax.read_terms ctxt1
-      |> Syntax.check_terms ctxt1;
+      |> Syntax.read_terms ctxt1;
 
     val term_insts' = map2 (fn (xi, _) => fn t => (xi, t)) term_insts terms;
 
@@ -149,9 +147,7 @@
 
     val term_insts =
       map (the_list o (Option.map Parse_Tools.the_parse_val)) insts'
-      |> burrow (Syntax.read_terms ctxt1
-        #> Syntax.check_terms ctxt1
-        #> Variable.export_terms ctxt1 ctxt)
+      |> burrow (Syntax.read_terms ctxt1 #> Variable.export_terms ctxt1 ctxt)
       |> map (try the_single);
 
     val _ =