src/HOL/Bali/Basis.thy
changeset 27239 f2f42f9fa09d
parent 27226 5a3e5e46d977
child 30235 58d147683393
     1.1 --- a/src/HOL/Bali/Basis.thy	Mon Jun 16 17:56:08 2008 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Mon Jun 16 22:13:39 2008 +0200
     1.3 @@ -230,7 +230,7 @@
     1.4  ML {*
     1.5  fun sum3_instantiate ctxt thm = map (fn s =>
     1.6    simplify (Simplifier.local_simpset_of ctxt delsimps[@{thm not_None_eq}])
     1.7 -    (RuleInsts.read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
     1.8 +    (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?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