src/HOL/Fun.thy
changeset 17956 369e2af8ee45
parent 17877 67d5ab1cb0d8
child 18154 0c05abaf6244
     1.1 --- a/src/HOL/Fun.thy	Fri Oct 21 18:14:32 2005 +0200
     1.2 +++ b/src/HOL/Fun.thy	Fri Oct 21 18:14:34 2005 +0200
     1.3 @@ -497,7 +497,7 @@
     1.4        (fn sg => fn ss => fn t =>
     1.5          case find_double t of (T, NONE) => NONE
     1.6          | (T, SOME rhs) =>
     1.7 -            SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
     1.8 +            SOME (Goal.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
     1.9  end;
    1.10  Addsimprocs[fun_upd2_simproc];
    1.11