src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
changeset 48408 5493e67982ee
parent 48406 b002cc16aa99
child 50053 fea589c8583e
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:43:51 2012 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    val mepo_suggested_facts :
     1.5      Proof.context -> params -> string -> int -> relevance_fudge option
     1.6      -> term list -> term -> fact list -> fact list
     1.7 -  val weight_mepo_facts : fact list -> (fact * real) list
     1.8 +  val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
     1.9  end;
    1.10  
    1.11  structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =