src/HOL/Tools/functor.ML

     val _ =
       if null (Term.add_vars (singleton
         (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 ()
       else error ("Illegal locally fixed type variable(s) in type: " ^ Syntax.string_of_typ ctxt T);
     fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts