# HG changeset patch
# User obua
# Date 1127560265 -7200
# Node ID 1539d18e3e9fe5ecadf4d3bd498b26e649b61a33
# Parent  da9a5efecde74f1524c5752ad58efc2cca2ed480
preliminary fix of HOL build problem

diff -r da9a5efecde7 -r 1539d18e3e9f src/HOL/SAT.thy
--- a/src/HOL/SAT.thy	Sat Sep 24 10:47:22 2005 +0200
+++ b/src/HOL/SAT.thy	Sat Sep 24 13:11:05 2005 +0200
@@ -16,6 +16,7 @@
 
 begin
 
+(*
 ML {* structure sat = SATFunc(structure cnf_struct = cnf); *}
 
 method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
@@ -24,7 +25,7 @@
 method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
   "SAT solver (with definitional CNF)"
 
-(*
+
 method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *}
   "Transforming hypotheses in a goal into CNF"