src/HOL/Bali/Basis.thy
changeset 27226 5a3e5e46d977
parent 27153 56b6cdce22f1
child 27239 f2f42f9fa09d
     1.1 --- a/src/HOL/Bali/Basis.thy	Mon Jun 16 17:54:35 2008 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Mon Jun 16 17:54:36 2008 +0200
     1.3 @@ -228,8 +228,9 @@
     1.4     "the_In1r" == "the_Inr \<circ> the_In1"
     1.5  
     1.6  ML {*
     1.7 -fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[@{thm not_None_eq}])
     1.8 - (Drule.read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"]
     1.9 +fun sum3_instantiate ctxt thm = map (fn s =>
    1.10 +  simplify (Simplifier.local_simpset_of ctxt delsimps[@{thm not_None_eq}])
    1.11 +    (RuleInsts.read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
    1.12  *}
    1.13  (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
    1.14