src/HOL/Tools/specification_package.ML
changeset 21116 be58cded79da
parent 20903 905effde63d9
child 21359 072e83a0b5bb
equal deleted inserted replaced
21115:f4e79a09c305 21116:be58cded79da
   138         val props'' = map proc_single props'
   138         val props'' = map proc_single props'
   139         val frees = map snd props''
   139         val frees = map snd props''
   140         val prop  = myfoldr HOLogic.mk_conj (map fst props'')
   140         val prop  = myfoldr HOLogic.mk_conj (map fst props'')
   141         val cprop = cterm_of thy (HOLogic.mk_Trueprop prop)
   141         val cprop = cterm_of thy (HOLogic.mk_Trueprop prop)
   142 
   142 
   143         val (prop_thawed,vmap) = Type.varify (prop,[])
   143         val (vmap, prop_thawed) = Type.varify [] prop
   144         val thawed_prop_consts = collect_consts (prop_thawed,[])
   144         val thawed_prop_consts = collect_consts (prop_thawed,[])
   145         val (altcos,overloaded) = Library.split_list cos
   145         val (altcos,overloaded) = Library.split_list cos
   146         val (names,sconsts) = Library.split_list altcos
   146         val (names,sconsts) = Library.split_list altcos
   147         val consts = map (term_of o Thm.read_cterm thy o rpair TypeInfer.logicT) sconsts
   147         val consts = map (term_of o Thm.read_cterm thy o rpair TypeInfer.logicT) sconsts
   148         val _ = assert (not (Library.exists (not o Term.is_Const) consts))
   148         val _ = assert (not (Library.exists (not o Term.is_Const) consts))
   149                        "Specification: Non-constant found as parameter"
   149                        "Specification: Non-constant found as parameter"
   150 
   150 
   151         fun proc_const c =
   151         fun proc_const c =
   152             let
   152             let
   153                 val c' = fst (Type.varify (c,[]))
   153                 val (_, c') = Type.varify [] c
   154                 val (cname,ctyp) = dest_Const c'
   154                 val (cname,ctyp) = dest_Const c'
   155             in
   155             in
   156                 case List.filter (fn t => let val (name,typ) = dest_Const t
   156                 case List.filter (fn t => let val (name,typ) = dest_Const t
   157                                      in name = cname andalso Sign.typ_equiv thy (typ, ctyp)
   157                                      in name = cname andalso Sign.typ_equiv thy (typ, ctyp)
   158                                      end) thawed_prop_consts of
   158                                      end) thawed_prop_consts of