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/proofterm.ML
changeset 19012 2577ac76cdc6
parent 18928 042608ffa2ec
child 19222 111ba44c66b2 
--- a/src/Pure/proofterm.ML	Sat Feb 11 17:17:45 2006 +0100
+++ b/src/Pure/proofterm.ML	Sat Feb 11 17:17:47 2006 +0100
@@ -913,7 +913,7 @@
             val prop = (case prf of PThm (_, _, prop, _) => prop | PAxm (_, prop, _) => prop
               | Oracle (_, prop, _) => prop | _ => error "shrink: proof not in normal form");
             val vs = vars_of prop;
-            val (ts', ts'') = splitAt (length vs, ts)
+            val (ts', ts'') = chop (length vs) ts;
             val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
             val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
               insert (op =) ixn (case AList.lookup (op =) insts ixn of
isabelle