List.partition;
authorwenzelm
Sat May 20 23:36:55 2006 +0200 (2006-05-20)
changeset 1968683611262823e
parent 19685 4477003648cc
child 19687 0a7c6d78ad6b
List.partition;
src/HOL/Import/proof_kernel.ML
src/HOL/Tools/recdef_package.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Sat May 20 23:36:53 2006 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat May 20 23:36:55 2006 +0200
     1.3 @@ -772,7 +772,7 @@
     1.4  	    mk_proof (PTyDef(seg,protect_tyname name,x2p p))
     1.5  	  | x2p (xml as Elem("poracle",[],chldr)) =
     1.6  	    let
     1.7 -		val (oracles,terms) = Library.partition (fn (Elem("oracle",_,_)) => true | _ => false) chldr
     1.8 +		val (oracles,terms) = List.partition (fn (Elem("oracle",_,_)) => true | _ => false) chldr
     1.9  		val ors = map (fn (Elem("oracle",[("n",name)],[])) => name | xml => raise ERR "x2p" "bad oracle") oracles
    1.10  		val (c,asl) = case terms of
    1.11  				  [] => raise ERR "x2p" "Bad oracle description"
     2.1 --- a/src/HOL/Tools/recdef_package.ML	Sat May 20 23:36:53 2006 +0200
     2.2 +++ b/src/HOL/Tools/recdef_package.ML	Sat May 20 23:36:55 2006 +0200
     2.3 @@ -80,7 +80,7 @@
     2.4  fun del_cong raw_thm congs =
     2.5    let
     2.6      val (c, thm) = prep_cong raw_thm;
     2.7 -    val (del, rest) = Library.partition (Library.equal c o fst) congs;
     2.8 +    val (del, rest) = List.partition (Library.equal c o fst) congs;
     2.9    in if null del then (warning ("No recdef congruence rule for " ^ quote c); congs) else rest end;
    2.10  
    2.11  val add_congs = foldr (uncurry add_cong);