--- a/src/HOL/Tools/functor.ML Fri Jul 29 20:38:39 2016 +0200
+++ b/src/HOL/Tools/functor.ML Sat Jul 30 21:10:02 2016 +0200
@@ -190,7 +190,7 @@
(Variable.export_terms (Variable.auto_fixes input_mapper ctxt) ctxt) input_mapper) [])
then ()
else error ("Illegal locally free variable(s) in term: "
- ^ Syntax.string_of_term ctxt input_mapper);;
+ ^ Syntax.string_of_term ctxt input_mapper);
val mapper = singleton (Variable.polymorphic ctxt) input_mapper;
val _ =
if null (Term.add_tfreesT (fastype_of mapper) []) then ()