src/HOL/Tools/meson.ML
changeset 32960 69916a850301
parent 32955 4a78daeb012b
child 33222 89ced80833ac
     1.1 --- a/src/HOL/Tools/meson.ML	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -266,21 +266,21 @@
     1.4    fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
     1.5      | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
     1.6      | signed_nclauses b (Const("op &",_) $ t $ u) =
     1.7 -	if b then sum (signed_nclauses b t) (signed_nclauses b u)
     1.8 -	     else prod (signed_nclauses b t) (signed_nclauses b u)
     1.9 +        if b then sum (signed_nclauses b t) (signed_nclauses b u)
    1.10 +             else prod (signed_nclauses b t) (signed_nclauses b u)
    1.11      | signed_nclauses b (Const("op |",_) $ t $ u) =
    1.12 -	if b then prod (signed_nclauses b t) (signed_nclauses b u)
    1.13 -	     else sum (signed_nclauses b t) (signed_nclauses b u)
    1.14 +        if b then prod (signed_nclauses b t) (signed_nclauses b u)
    1.15 +             else sum (signed_nclauses b t) (signed_nclauses b u)
    1.16      | signed_nclauses b (Const("op -->",_) $ t $ u) =
    1.17 -	if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
    1.18 -	     else sum (signed_nclauses (not b) t) (signed_nclauses b u)
    1.19 +        if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
    1.20 +             else sum (signed_nclauses (not b) t) (signed_nclauses b u)
    1.21      | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
    1.22 -	if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
    1.23 -	    if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
    1.24 -			  (prod (signed_nclauses (not b) u) (signed_nclauses b t))
    1.25 -		 else sum (prod (signed_nclauses b t) (signed_nclauses b u))
    1.26 -			  (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
    1.27 -	else 1
    1.28 +        if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
    1.29 +            if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
    1.30 +                          (prod (signed_nclauses (not b) u) (signed_nclauses b t))
    1.31 +                 else sum (prod (signed_nclauses b t) (signed_nclauses b u))
    1.32 +                          (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
    1.33 +        else 1
    1.34      | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
    1.35      | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
    1.36      | signed_nclauses _ _ = 1; (* literal *)
    1.37 @@ -347,9 +347,9 @@
    1.38            | _ => nodups ctxt th :: ths  (*no work to do*)
    1.39        and cnf_nil th = cnf_aux (th,[])
    1.40        val cls = 
    1.41 -	    if too_many_clauses (SOME ctxt) (concl_of th)
    1.42 -	    then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
    1.43 -	    else cnf_aux (th,ths)
    1.44 +            if too_many_clauses (SOME ctxt) (concl_of th)
    1.45 +            then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
    1.46 +            else cnf_aux (th,ths)
    1.47    in  (cls, !ctxtr)  end;
    1.48  
    1.49  fun make_cnf skoths th ctxt = cnf skoths ctxt (th, []);