Lines Matching refs:body
642 body:(Token.T list * TheoryData.thy_body)
676 body:(Token.T list * TheoryData.thy_body) list};
691 #> (fn (((h,a),b),_) => Thy {header=h,args=a,body=b}));
793 fun xml name attrs body = XML.Elem ((name,attrs),body);
794 fun xml' name body attrs = xml name attrs body;
827 (body : (Token.T list * 'b) list) =
828 let val btoks = List.map #1 body |> flat
970 HOLogic.dest_eq |> (fn (head,body) =>
971 (strip_comb head,body)) end) eqs
1062 fn Instantiation (arity,body) =>
1066 val (begin_,end_) = extract_context toks body
1069 List.foldl xml_of_body_elem ((s1,trans),[]) body
1100 fn Locale ((name,(parents,ctxt)),body) =>
1101 let val (begin_,end_) = extract_context toks body
1104 List.foldl xml_of_body_elem ((s1,trans),[]) body
1115 fn Class ((name,(parents,ctxt)),body) =>
1116 let val (begin_,end_) = extract_context toks body
1119 List.foldl xml_of_body_elem ((s1,trans),[]) body
1218 |> (fn (head,body) =>
1220 (f,vs) => ((dest_Free f,vs),body))
1272 fun xml_of_body state body =
1273 List.foldl xml_of_body_elem (state,[]) body;
1281 val (Thy {header,args=(th,h),body}) =
1298 val (s',body'') = xml_of_body (s,t) body
1303 val body' = [body'' |> List.rev |> xml "Body" []]
1304 in thys@[xml "Thy" (name@header') (imports@keywords@body')] end;