src/Pure/Isar/locale.ML

 
     val args = map Logic.mk_type extraTs @ map Free xs;
     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), []))
       |> Theory.add_consts_i [(bname, predT, Syntax.NoSyn)]
       |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];