src/HOL/Tools/function_package/fundef_package.ML
changeset 19611 da2a0014c461
parent 19585 70a1ce3b23ae
child 19617 7cb4b67d4b97
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu May 11 11:11:05 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu May 11 15:46:40 2006 +0200
     1.3 @@ -26,14 +26,12 @@
     1.4  val True_implies = thm "True_implies"
     1.5  
     1.6  
     1.7 -fun fundef_afterqed congs curry_info name data natts thmss thy =
     1.8 +fun fundef_afterqed congs curry_info name data names atts thmss thy =
     1.9      let
    1.10  	val (complete_thm :: compat_thms) = map hd thmss
    1.11  	val fundef_data = FundefProof.mk_partial_rules_curried thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
    1.12  	val FundefResult {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
    1.13  
    1.14 -	val (names, attsrcs) = split_list natts
    1.15 -	val atts = map (map (Attrib.attribute thy)) attsrcs
    1.16  
    1.17  	val Prep {names = Names {acc_R=accR, ...}, ...} = data
    1.18  	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    1.19 @@ -55,19 +53,25 @@
    1.20  	add_fundef_data name fundef_data thy
    1.21      end
    1.22  
    1.23 -fun add_fundef eqns_atts thy =
    1.24 +fun gen_add_fundef prep_att eqns_atts thy =
    1.25      let
    1.26  	val (natts, eqns) = split_list eqns_atts
    1.27 +	val (names, raw_atts) = split_list natts
    1.28 +
    1.29 +	val atts = map (map (prep_att thy)) raw_atts
    1.30  
    1.31  	val congs = get_fundef_congs (Context.Theory thy)
    1.32  
    1.33 -	val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs (map (Sign.read_prop thy) eqns) thy
    1.34 +	val t_eqns = map (Sign.read_prop thy) eqns
    1.35 +			 |> map (term_of o cterm_of thy) (* HACK to prevent strange things from happening with abbreviations *)
    1.36 +
    1.37 +	val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs t_eqns thy
    1.38  	val Prep {complete, compat, ...} = data
    1.39  
    1.40  	val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
    1.41      in
    1.42  	thy |> ProofContext.init
    1.43 -	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs curry_info name data natts) NONE ("", [])
    1.44 +	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs curry_info name data names atts) NONE ("", [])
    1.45  	    (map (fn t => (("", []), [(t, [])])) props)
    1.46      end
    1.47  
    1.48 @@ -152,6 +156,8 @@
    1.49      end	
    1.50  
    1.51  
    1.52 +val add_fundef = gen_add_fundef Attrib.attribute
    1.53 +
    1.54  
    1.55  
    1.56  (* congruence rules *)