src/HOL/Bali/Basis.thy
changeset 27153 56b6cdce22f1
parent 26349 7f5a2f6d9119
child 27226 5a3e5e46d977
     1.1 --- a/src/HOL/Bali/Basis.thy	Wed Jun 11 18:01:36 2008 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Wed Jun 11 18:02:00 2008 +0200
     1.3 @@ -229,7 +229,7 @@
     1.4  
     1.5  ML {*
     1.6  fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[@{thm not_None_eq}])
     1.7 - (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"]
     1.8 + (Drule.read_instantiate [("t","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