src/HOL/Bali/Basis.thy

--- a/src/HOL/Bali/Basis.thy	Sat Jan 25 21:52:04 2014 +0100
+++ b/src/HOL/Bali/Basis.thy	Sat Jan 25 22:06:07 2014 +0100
@@ -181,7 +181,7 @@
 ML {*
 fun sum3_instantiate ctxt thm = map (fn s =>
   simplify (ctxt delsimps [@{thm not_None_eq}])
-    (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
+    (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " x")] ["x"] thm)) ["1l","2","3","1r"]
 *}
 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)