src/HOL/Bali/Basis.thy
changeset 55143 04448228381d
parent 52037 837211662fb8
child 55151 f331472f1027
     1.1 --- a/src/HOL/Bali/Basis.thy	Sat Jan 25 21:52:04 2014 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Sat Jan 25 22:06:07 2014 +0100
     1.3 @@ -181,7 +181,7 @@
     1.4  ML {*
     1.5  fun sum3_instantiate ctxt thm = map (fn s =>
     1.6    simplify (ctxt delsimps [@{thm not_None_eq}])
     1.7 -    (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
     1.8 +    (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " x")] ["x"] thm)) ["1l","2","3","1r"]
     1.9  *}
    1.10  (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
    1.11