src/HOL/OrderedGroup.thy
changeset 32010 cb1a1c94b4cd
parent 31902 862ae16a799d
child 32075 e8e0fb5da77a
     1.1 --- a/src/HOL/OrderedGroup.thy	Wed Jul 15 23:11:57 2009 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Wed Jul 15 23:48:21 2009 +0200
     1.3 @@ -1380,7 +1380,7 @@
     1.4          if termless_agrp (y, x) then SOME ac2 else NONE
     1.5      | solve_add_ac thy _ _ = NONE
     1.6  in
     1.7 -  val add_ac_proc = Simplifier.simproc (the_context ())
     1.8 +  val add_ac_proc = Simplifier.simproc @{theory}
     1.9      "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
    1.10  end;
    1.11