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/Isar/locale.ML
changeset 18358 0a733e11021a
parent 18343 e36238ac5359
child 18377 0e1d025d57b3 
--- a/src/Pure/Isar/locale.ML	Tue Dec 06 06:22:14 2005 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Dec 06 09:04:09 2005 +0100
@@ -1589,7 +1589,7 @@
     val head = Term.list_comb (Const (name, predT), args);
     val statement = ObjectLogic.ensure_propT thy head;
 
-    val (defs_thy, [pred_def]) =
+    val ([pred_def], defs_thy) =
       thy
       |> (if bodyT <> propT then I else
         Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
isabelle