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.
TFL/tfl.sml
changeset 6397 e70ae9b575cc
parent 6092 d9db67970c73
child 6498 1ebbe18fe236 
--- a/TFL/tfl.sml	Wed Mar 17 17:19:18 1999 +0100
+++ b/TFL/tfl.sml	Wed Mar 17 17:20:36 1999 +0100
@@ -336,7 +336,7 @@
 	                  (wfrec $ map_term_types poly_tvars R) 
 	              $ functional
      val (def_term, _) = 
-	 Sign.infer_types (sign_of thy) (K None) (K None) [] false
+	 Sign.infer_types (Theory.sign_of thy) (K None) (K None) [] false
 	       ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], 
 		propT)
   in  PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy  end
isabelle