src/Pure/raw_simplifier.ML
changeset 55377 d79c057c68f0
parent 55316 885500f4aa6a
child 55635 00e900057b38
     1.1 --- a/src/Pure/raw_simplifier.ML	Sun Feb 09 21:37:27 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Mon Feb 10 13:04:08 2014 +0100
     1.3 @@ -375,11 +375,7 @@
     1.4  
     1.5  fun simpset_map ctxt f ss = ctxt |> map_simpset (K ss) |> f |> Context.Proof |> Simpset.get;
     1.6  
     1.7 -fun put_simpset ss = map_simpset (fn context_ss =>
     1.8 -  let
     1.9 -    val Simpset ({rules, prems, ...}, ss2) = ss;  (* FIXME prems from context (!?) *)
    1.10 -    val Simpset ({depth, ...}, _) = context_ss;
    1.11 -  in Simpset (make_ss1 (rules, prems, depth), ss2) end);
    1.12 +fun put_simpset ss = map_simpset (K ss);
    1.13  
    1.14  val empty_simpset = put_simpset empty_ss;
    1.15