Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/goal.ML
changeset 20260 990dbc007ca6
parent 20250 c3f209752749
child 20290 3f886c176c9b 
--- a/src/Pure/goal.ML	Sun Jul 30 21:28:51 2006 +0200
+++ b/src/Pure/goal.ML	Sun Jul 30 21:28:52 2006 +0200
@@ -153,7 +153,7 @@
   (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
    else if n = 1 then Seq.single (Thm.cprem_of st i)
    else Seq.single (foldr1 Conjunction.mk_conjunction (map (Thm.cprem_of st) (i upto i + n - 1))))
-  |> Seq.map (Thm.adjust_maxidx #> init);
+  |> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init);
 
 fun retrofit i n st' st =
   (if n = 1 then st
isabelle