src/HOL/Bali/Basis.thy
changeset 22633 a47e4fd7ebc1
parent 22578 b0eb5652f210
child 22781 18fbba942a80
     1.1 --- a/src/HOL/Bali/Basis.thy	Wed Apr 11 08:28:13 2007 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Wed Apr 11 08:28:14 2007 +0200
     1.3 @@ -246,7 +246,7 @@
     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[not_None_eq])
     1.8 +fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[@{thm not_None_eq}])
     1.9   (read_instantiate [("t","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] *)