src/HOL/Tools/sat_funcs.ML
changeset 32231 95b8afcbb0ed
parent 32155 e2bf2f73b0c8
child 32232 6c394343360f
     1.1 --- a/src/HOL/Tools/sat_funcs.ML	Mon Jul 27 17:36:30 2009 +0200
     1.2 +++ b/src/HOL/Tools/sat_funcs.ML	Mon Jul 27 20:45:40 2009 +0200
     1.3 @@ -410,7 +410,7 @@
     1.4  (*      or "True"                                                            *)
     1.5  (* ------------------------------------------------------------------------- *)
     1.6  
     1.7 -fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
     1.8 +fun rawsat_tac i = OldGoals.METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
     1.9  
    1.10  (* ------------------------------------------------------------------------- *)
    1.11  (* pre_cnf_tac: converts the i-th subgoal                                    *)