# HG changeset patch
# User wenzelm
# Date 1434531431 -7200
# Node ID 54a3db2ed201b1b2c1ecd57da983c281362f477e
# Parent  db0f4f4c17c732cbf43bbc7fcd09b997a0a60ea2
avoid dynamic parsing of hardwired strings;

diff -r db0f4f4c17c7 -r 54a3db2ed201 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Tue Jun 16 20:50:00 2015 +0100
+++ b/src/HOL/Tools/Function/function.ML	Wed Jun 17 10:57:11 2015 +0200
@@ -156,9 +156,13 @@
     |> afterqed [[pattern_thm]]
   end
 
+val default_constraint_any = Type_Infer.anyT @{sort type};
+val default_constraint_any' = YXML.string_of_body (Term_XML.Encode.typ default_constraint_any);
+
 val add_function =
-  gen_add_function false Specification.check_spec (Type_Infer.anyT @{sort type})
-fun add_function_cmd a b c d int = gen_add_function int Specification.read_spec "_::type" a b c d
+  gen_add_function false Specification.check_spec default_constraint_any
+fun add_function_cmd a b c d int =
+  gen_add_function int Specification.read_spec default_constraint_any' a b c d
 
 fun gen_function do_print prep default_constraint fixspec eqns config lthy =
   let
@@ -171,8 +175,9 @@
   end
 
 val function =
-  gen_function false Specification.check_spec (Type_Infer.anyT @{sort type})
-fun function_cmd a b c int = gen_function int Specification.read_spec "_::type" a b c
+  gen_function false Specification.check_spec default_constraint_any
+fun function_cmd a b c int =
+  gen_function int Specification.read_spec default_constraint_any' a b c
 
 fun prepare_termination_proof prep_term raw_term_opt lthy =
   let