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/ZF/Tools/induct_tacs.ML
changeset 26939 1035c89b4c02
parent 26618 f3535afb58e8
child 27208 5fe899199f85 
--- a/src/ZF/Tools/induct_tacs.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Sun May 18 15:04:09 2008 +0200
@@ -120,7 +120,7 @@
     (*analyze the LHS of a case equation to get a constructor*)
     fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
       | const_of eqn = error ("Ill-formed case equation: " ^
-                              Sign.string_of_term thy eqn);
+                              Syntax.string_of_term_global thy eqn);
 
     val constructors =
         map (head_of o const_of o FOLogic.dest_Trueprop o
isabelle