src/HOL/Tools/Function/measure_functions.ML
changeset 67149 e61557884799
parent 59621 291934bac95e
     1.1 --- a/src/HOL/Tools/Function/measure_functions.ML	Wed Dec 06 19:34:59 2017 +0100
     1.2 +++ b/src/HOL/Tools/Function/measure_functions.ML	Wed Dec 06 20:43:09 2017 +0100
     1.3 @@ -15,10 +15,10 @@
     1.4  (** User-declared size functions **)
     1.5  
     1.6  fun mk_is_measure t =
     1.7 -  Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
     1.8 +  Const (\<^const_name>\<open>is_measure\<close>, fastype_of t --> HOLogic.boolT) $ t
     1.9  
    1.10  fun find_measures ctxt T =
    1.11 -  DEPTH_SOLVE (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems measure_function})) 1)
    1.12 +  DEPTH_SOLVE (resolve_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>measure_function\<close>)) 1)
    1.13      (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
    1.14       |> Thm.cterm_of ctxt |> Goal.init)
    1.15    |> Seq.map (Thm.prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
    1.16 @@ -30,17 +30,17 @@
    1.17  fun constant_0 T = Abs ("x", T, HOLogic.zero)
    1.18  fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
    1.19  
    1.20 -fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
    1.21 +fun mk_funorder_funs (Type (\<^type_name>\<open>Sum_Type.sum\<close>, [fT, sT])) =
    1.22    map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
    1.23    @ map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
    1.24    | mk_funorder_funs T = [ constant_1 T ]
    1.25  
    1.26 -fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
    1.27 +fun mk_ext_base_funs ctxt (Type (\<^type_name>\<open>Sum_Type.sum\<close>, [fT, sT])) =
    1.28      map_product (Sum_Tree.mk_sumcase fT sT HOLogic.natT)
    1.29        (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
    1.30    | mk_ext_base_funs ctxt T = find_measures ctxt T
    1.31  
    1.32 -fun mk_all_measure_funs ctxt (T as Type (@{type_name Sum_Type.sum}, _)) =
    1.33 +fun mk_all_measure_funs ctxt (T as Type (\<^type_name>\<open>Sum_Type.sum\<close>, _)) =
    1.34      mk_ext_base_funs ctxt T @ mk_funorder_funs T
    1.35    | mk_all_measure_funs ctxt T = find_measures ctxt T
    1.36