src/Pure/goal.ML
changeset 20260 990dbc007ca6
parent 20250 c3f209752749
child 20290 3f886c176c9b
     1.1 --- a/src/Pure/goal.ML	Sun Jul 30 21:28:51 2006 +0200
     1.2 +++ b/src/Pure/goal.ML	Sun Jul 30 21:28:52 2006 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4    (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
     1.5     else if n = 1 then Seq.single (Thm.cprem_of st i)
     1.6     else Seq.single (foldr1 Conjunction.mk_conjunction (map (Thm.cprem_of st) (i upto i + n - 1))))
     1.7 -  |> Seq.map (Thm.adjust_maxidx #> init);
     1.8 +  |> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init);
     1.9  
    1.10  fun retrofit i n st' st =
    1.11    (if n = 1 then st