src/HOL/Tools/Function/function_common.ML
changeset 56245 84fc7dfa3cd4
parent 54740 91f54d386680
child 56254 a2dd9200854d
     1.1 --- a/src/HOL/Tools/Function/function_common.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Tools/Function/function_common.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -280,8 +280,8 @@
     1.4  fun split_def ctxt check_head geq =
     1.5    let
     1.6      fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
     1.7 -    val qs = Term.strip_qnt_vars "all" geq
     1.8 -    val imp = Term.strip_qnt_body "all" geq
     1.9 +    val qs = Term.strip_qnt_vars @{const_name Pure.all} geq
    1.10 +    val imp = Term.strip_qnt_body @{const_name Pure.all} geq
    1.11      val (gs, eq) = Logic.strip_horn imp
    1.12  
    1.13      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)