Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
stating more explicitly our expectation that these two terms have the same term structure
authorbulwahn
Fri, 09 Sep 2011 14:43:50 +0200
changeset 44855 f4a6786057d9
parent 44854 0b3d3570ab31
child 44856 3d44712a5f66
stating more explicitly our expectation that these two terms have the same term structure
src/Tools/Code/code_thingol.ML file | annotate | diff | comparison | revisions 
--- a/src/Tools/Code/code_thingol.ML	Fri Sep 09 12:33:09 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Sep 09 14:43:50 2011 +0200
@@ -596,7 +596,9 @@
     end
   | annotate_term (Abs (_, _, t1) , Abs (x, T, t)) tvar_names =
     apfst (fn t => Abs (x, T, t)) (annotate_term (t1, t) tvar_names)
-  | annotate_term (_, t) tvar_names = (t, tvar_names)
+  | annotate_term (Free _, t as Free _) tvar_names = (t, tvar_names)
+  | annotate_term (Var _, t as Var _) tvar_names = (t, tvar_names)
+  | annotate_term (Bound   _, t as Bound _) tvar_names = (t, tvar_names)
 
 fun annotate_eqns thy (c, ty) eqns = 
   let
isabelle