src/HOL/Tools/Function/termination.ML
changeset 54742 7a86358a3c0b
parent 52732 b4da1f2ec73f
child 55968 94242fa87638
     1.1 --- a/src/HOL/Tools/Function/termination.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Tools/Function/termination.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -305,7 +305,7 @@
     1.4    in
     1.5      (PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
     1.6       THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
     1.7 -     THEN rewrite_goal_tac Un_aci_simps 1) st  (* eliminate duplicates *)
     1.8 +     THEN rewrite_goal_tac ctxt Un_aci_simps 1) st  (* eliminate duplicates *)
     1.9    end
    1.10  
    1.11  end