src/Pure/Tools/codegen_func.ML
changeset 23418 c195f6f13769
parent 23249 9ef65be6bb2a
     1.1 --- a/src/Pure/Tools/codegen_func.ML	Tue Jun 19 23:15:23 2007 +0200
     1.2 +++ b/src/Pure/Tools/codegen_func.ML	Tue Jun 19 23:15:27 2007 +0200
     1.3 @@ -238,9 +238,9 @@
     1.4      fun burrow_thms f [] = []
     1.5        | burrow_thms f thms =
     1.6            thms
     1.7 -          |> Conjunction.intr_list
     1.8 +          |> Conjunction.intr_balanced
     1.9            |> f
    1.10 -          |> Conjunction.elim_list;
    1.11 +          |> Conjunction.elim_balanced (length thms)
    1.12    in
    1.13      thms
    1.14      |> burrow_thms (canonical_tvars purify_tvar)