src/HOL/Bali/Basis.thy
changeset 55151 f331472f1027
parent 55143 04448228381d
child 55414 eab03e9cee8a
     1.1 --- a/src/HOL/Bali/Basis.thy	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Sun Jan 26 13:45:40 2014 +0100
     1.3 @@ -179,9 +179,11 @@
     1.4    where "the_In1r \<equiv> the_Inr \<circ> the_In1"
     1.5  
     1.6  ML {*
     1.7 -fun sum3_instantiate ctxt thm = map (fn s =>
     1.8 -  simplify (ctxt delsimps [@{thm not_None_eq}])
     1.9 -    (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " x")] ["x"] thm)) ["1l","2","3","1r"]
    1.10 +fun sum3_instantiate ctxt thm =
    1.11 +  map (fn s =>
    1.12 +    simplify (ctxt delsimps @{thms not_None_eq})
    1.13 +      (Rule_Insts.read_instantiate ctxt [(("t", 0), "In" ^ s ^ " x")] ["x"] thm))
    1.14 +    ["1l","2","3","1r"]
    1.15  *}
    1.16  (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
    1.17