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/Syntax/syntax_phases.ML
changeset 55955 e8f1bf005661
parent 55954 a29aefc88c8d
child 55956 94d384d621b0 
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 13:44:01 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 14:38:54 2014 +0100
@@ -224,7 +224,7 @@
 fun decode_const ctxt c =
   let
     val (Const (c', _), _) =
-      Proof_Context.check_const ctxt {proper = true, strict = false} dummyT (c, Position.none);
+      Proof_Context.check_const ctxt {proper = true, strict = false} (c, Position.none);
   in c' end;
 
 fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
isabelle