# HG changeset patch
# User blanchet
# Date 1277476147 -7200
# Node ID 512cf962d54cb2ffa41ab5f352aad0c114d74a73
# Parent  cfc5e281740f8519134ec9b9a70fa257f57761c9
get rid of type alias

diff -r cfc5e281740f -r 512cf962d54c src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Jun 25 16:27:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Jun 25 16:29:07 2010 +0200
@@ -13,7 +13,6 @@
   type kind = Sledgehammer_FOL_Clause.kind
   type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
   type arity_clause = Sledgehammer_FOL_Clause.arity_clause
-  type polarity = bool
 
   datatype combtyp =
     TyVar of name |
@@ -23,7 +22,7 @@
     CombConst of name * combtyp * combtyp list (* Const and Free *) |
     CombVar of name * combtyp |
     CombApp of combterm * combterm
-  datatype literal = Literal of polarity * combterm
+  datatype literal = Literal of bool * combterm
   datatype hol_clause =
     HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
                   literals: literal list, ctypes_sorts: typ list}
@@ -57,8 +56,6 @@
 (* data types for typed combinator expressions        *)
 (******************************************************)
 
-type polarity = bool
-
 datatype combtyp =
   TyVar of name |
   TyFree of name |
@@ -69,7 +66,7 @@
   CombVar of name * combtyp |
   CombApp of combterm * combterm
 
-datatype literal = Literal of polarity * combterm;
+datatype literal = Literal of bool * combterm
 
 datatype hol_clause =
   HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
@@ -149,10 +146,8 @@
       in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
   | combterm_of _ (t as Abs _) = raise Fail "HOL clause: Abs"
 
-fun predicate_of thy ((@{const Not} $ P), polarity) =
-    predicate_of thy (P, not polarity)
-  | predicate_of thy (t, polarity) =
-    (combterm_of thy (Envir.eta_contract t), polarity)
+fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
+  | predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos)
 
 fun literals_of_term1 args thy (@{const Trueprop} $ P) =
     literals_of_term1 args thy P