src/HOL/Bali/Basis.thy
changeset 32149 ef59550a55d3
parent 30235 58d147683393
child 32367 a508148f7c25
     1.1 --- a/src/HOL/Bali/Basis.thy	Thu Jul 23 18:44:08 2009 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Thu Jul 23 18:44:09 2009 +0200
     1.3 @@ -229,7 +229,7 @@
     1.4  
     1.5  ML {*
     1.6  fun sum3_instantiate ctxt thm = map (fn s =>
     1.7 -  simplify (Simplifier.local_simpset_of ctxt delsimps[@{thm not_None_eq}])
     1.8 +  simplify (simpset_of ctxt delsimps[@{thm not_None_eq}])
     1.9      (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
    1.10  *}
    1.11  (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)